1 set "baseuri" "cic:/matita/tests/first/".
3 inductive nat : Set \def
7 inductive eq (A:Set): A \to A \to Prop \def
8 refl: \forall x:A.eq A x x.
10 inductive list (A:Set) : Set \def
12 | cons : A \to list A \to list A.
14 let rec list_len (A:Set) (l:list A) on l \def
18 | (cons a tl) \Rightarrow S (list_len A tl)].
20 theorem stupid: \forall A:Set.eq ? (list_len A (nil ?)) O.