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(_,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 rec append : forall 'a. 'a list -> 'a list -> 'a list =
          fun ['a] (m n : 'a list) =>
            match m with
              | Nil => n
              | Cons(_,xs) => Cons['a](??x__7__10??,append [???] xs n)
            end


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 rec append_bis : forall 'a. 'a list -> 'a list -> 'a list =
          fun ['a] (m n : 'a list) =>
            match m with
              | Nil => n
              | Cons(_,xs) => append_bis [???] xs Cons['a](??x__19__22??,n)
            end