type nat = Z | S of nat
type 'a list = Nil | Cons of 'a * 'a list

let rec length2 : forall 'a. 'a list -> nat = fun ['a] (l : 'a list) =>
  match l with
    | Nil => Z
    | Cons(x,xs) => S(S(length2 ['a] xs))
  end

let forall 'a ornament length2 ['a] : 'a list -> nat