Recursion in Hippogriff at small types

def List (a : Type) : Type := sum
  'empty
  'cons a (List a)
end

def map (a : Type) (b : Type) (f : a -> b) (xs : List a) : List b := match xs
  'empty => 'empty
  'cons x xs => 'cons (f x) (rec (map a b f xs))
end

def main : List Int := map Int Int (x => x + 1) ('cons 1 'empty)

\[\ms{rec} \colon (A \colon \ms{Ty}_k) \to \ms{IsSmall}\,A \to \triangleright(\ms{El}_k\,A) \to \ms{El}_k\,A\]