+inductive listn (A:Type) : nat \to Type \def
+ | Nil : listn A O
+ | Next : \forall n.\forall l:listn A n.\forall a:A.listn A (S n).
+
+definition if : \forall A:Type.\forall b:bool.\forall a,c:A.A \def
+ \lambda A,b,a,c.
+ match b with
+ [ true \Rightarrow a
+ | false \Rightarrow c].
+
+let rec ith (A:Type) (n,m:nat) (dummy:A) (l:listn A n) on l \def
+ match l with
+ [ Nil \Rightarrow dummy
+ | (Next w l x) \Rightarrow if A (eqb w m) x (ith A w m dummy l)].
+
+definition listn2function:
+ \forall A:Type.\forall dummy:A.\forall n.listn A n \to nat \to A
+\def
+ \lambda A,dummy,n,l,m.ith A n m dummy l.
+
+definition natlist2map: ? \def listn2function nat O.
+
+coercion cic:/matita/tests/coercions/natlist2map.con 1.
+definition map: \forall n:nat.\forall l:listn nat n. nat \to nat \def
+ \lambda n:nat.\lambda l:listn nat n.\lambda m:nat.l m.
+
+definition church: nat \to nat \to nat \def times.
+
+coercion cic:/matita/tests/coercions/church.con 1.
+lemma foo0 : ∀n:nat. n n = n * n.
+intros; reflexivity;
+qed.
+lemma foo01 : ∀n:nat. n n n = n * n * n.
+intros; reflexivity;
+qed.