:l Bool.pi

Nat : Type;
Nat = (l : { z s }) * case l of {
                           z -> Unit
			 | s -> Rec [Nat] };

zero : Nat;
zero = ('z,'unit);

succ : Nat -> Nat;
succ = \ n -> ('s,fold n);

one : Nat;
one = succ zero;

two : Nat;
two = succ one;

add : Nat -> Nat -> Nat;
add = \ m n -> split m with (lm , m') ->
                 ! case lm of {
		     z -> [n]
 		   | s -> [succ (add (unfold m') n)] };


eqNat : Nat -> Nat -> Bool;
eqNat = \ m n -> split m with (lm , m') ->
                  split n with (ln , n') ->
                  ! case lm of {
		     z -> case ln of {
		             z -> ['true]
			   | s -> ['false] }
	           | s -> case ln of {
		             z -> ['false]
			   | s -> [eqNat (unfold m') (unfold n')] } };

EqNat : Nat -> Nat -> Type;
EqNat = \ m n -> T (eqNat m n);

reflNat : (n:Nat) -> EqNat n n;
reflNat = \ n -> split n with (ln , n') ->
       	        ! case ln of {
		     z -> ['unit]
		   | s -> [reflNat (unfold n')] };

substNat : (P : Nat -> Type)
      -> (m : Nat) -> (n : Nat)
      -> (EqNat m n)
      -> P m -> P n;
substNat = \ P m n q x ->
              split m with (lm , m') ->
              split n with (ln , n') ->
                 ! case lm of {
		     z -> case ln of {
		             z -> case m' of {
			             unit -> case n' of {
				                unit -> [x]}}
			   | s -> case q of {}}
	           | s -> case ln of {
		             z -> case q of {}
			   | s -> [unfold m' as m' ->
                                   unfold n' as n' ->
                                   substNat (\ i -> P (succ i)) m' n' q x]}};


symNat : (m:Nat) -> (n:Nat) -> EqNat m n -> EqNat n m;
symNat = \ m n p -> substNat (\ i -> EqNat i m) m n p (reflNat m);

transNat : (i:Nat) -> (j:Nat) -> (k:Nat) ->
      EqNat i j -> EqNat j k -> EqNat i k;
transNat = \ i j k p q -> substNat (\ x -> EqNat i x) j k q p;

addCom0 : (n:Nat) -> EqNat n (add n zero);
addCom0 = \ n -> split n with (ln , n') ->
	         ! case ln of {
		      z -> case n' of {
		              unit -> [reflNat zero]}
	            | s -> [addCom0 (unfold n')] };

addComS : (m:Nat) -> (n:Nat) ->
	  (EqNat  (add (succ m) n) (add m (succ n)));
addComS = \ m n -> split m with (lm , m') ->
	           ! case lm of {
		       z -> [reflNat (succ n)]
		     | s -> [addComS (unfold m') n] };

addCom : (m:Nat) -> (n:Nat) ->
	  (EqNat (add m n) (add n m));
addCom = \ m n ->  split m with (lm , m') ->
	           ! case lm of {
		       z ->  case m' of {
		                unit -> [addCom0 n] }
		     | s -> [unfold m' as m' ->
                             transNat (add (succ m') n) (add (succ n) m') (add n (succ m'))
		                      (addCom m' n) (addComS n m')] };