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

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

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