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

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

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

let rec add : nat -> nat -> nat = fun (m n : nat) =>
  match m with
    | Z => n
    | S(m') => S (add m' n)
  end

let ornament append from add
  with forall +'a. {length ['a]} -> {length ['a]} -> {length ['a]}

let rec add_bis : nat -> nat -> nat = fun (m n : nat) => 
  match m with
    | Z => n
    | S(m') => add_bis m' (S(n))
end

let ornament append_bis from add_bis
  with forall +'a. {length ['a]} -> {length ['a]} -> {length ['a]}