Module ha Import id;

$[Nat : Set];
$[O : Nat];
$[s : Nat -> Nat];

$[Rec : {X|Set}X->(Nat->X->X)->Nat->X];

[[X:Set][x:X][f:Nat->X->X][n:Nat]
   Rec x f O ==> x
|| Rec x f (s n) ==> f n (Rec x f n)];

$[pa1 : {n:Nat}(Id O (s n))->False];

(* $[pa2 : {m,n:Nat}(Id (s m) (s n)) -> (Id m n)]; *)

(* note that 
pa2 : {m,n:Nat}(Id (s m) (s n)) -> (Id m n)
is derivable from Rec, Subst *)

$[Ind : {P:Nat->Prop}(P O)
	-> ({n:Nat}(P n)->(P (s n)))
	-> {n:Nat}(P n)];
[[P:Nat->Prop][x:P O][f:{n:Nat}(P n)->(P (s n))][n:Nat]
   Ind P x f O ==> x
|| Ind P x f (s n) ==> f n (Ind P x f n)];


[d = Rec O ([m:Nat][n:Nat]s (s n))];

[p = Rec O ([m:Nat][n:Nat]m)];

[add = Rec ([n:Nat]n) ([m:Nat][f:Nat -> Nat][n:Nat]s (f n))];