+
+Inductive nat : Set \def
+| O : nat
+| S : nat \to nat.
+
+Inductive list (A:Set) : Set \def
+| nil : list A
+| cons : A \to list A \to list A.
+
+Inductive bool: Set \def
+| true : bool
+| false : bool.
+
+
+
+
+let rec len (A:Set)(l:list A) on l : nat \def
+ match l:list with [
+ nil \Rightarrow O
+ | (cons e tl) \Rightarrow (S (len A tl))].
+
+let rec plus (n,m:nat) : nat \def
+ match n:nat with [
+ O \Rightarrow m
+ | (S x) \Rightarrow (S (plus x m)) ].
+
+let rec is_zero (n:nat) : bool \def
+ match n:nat with [
+ O \Rightarrow true
+ | (S x) \Rightarrow false].
+
+let rec nat_eq_dec (n,m:nat) : bool \def
+ match n:nat with [
+ O \Rightarrow
+ match m:nat with [
+ O \Rightarrow true
+ | (S x) \Rightarrow false]
+ | (S x) \Rightarrow
+ match m:nat with [
+ O \Rightarrow false
+ | (S y) \Rightarrow (nat_eq_dec x y)]
+ ].
+
+
+Coercion is_zero.
+Coercion len.
+
+Print Coer.
+Print Env.
+