Fixpoint enc (n : nat) :=
  lam(lam
  match n with
  | 0 ⇒ # 1
  | S n ⇒ # 0 (enc n)
  end).

Lemma enc_lam m :
  lambda (enc m).

Lemma enc_cls m :
  closed (enc m).


Lemma enc_proc m :
  proc (enc m).

Definition Zero : term := .\"z","s"; "z".
Definition Succ : term := .\"n","z","s"; "s" "n".


Lemma Succ_correct n : Succ (enc n) == enc (S n).

Definition Pred : term := .\"n"; "n" !Zero (.\"n"; "n").


Lemma Pred_correct n : Pred (enc n) == enc (pred n).

Definition Add := R (.\ "a", "n", "m"; "n" "m" (.\"n"; !Succ ("a" "n" "m"))).


Lemma Add_rec_0 m :
  Add Zero (enc m) == enc m.


Lemma Add_rec_S n m :
  Add (enc (S n)) (enc m) == Succ (Add (enc n) (enc m)).

Lemma Add_correct n m :
  Add (enc n) (enc m) == enc (n + m).

Definition Mul := R(.\ "Mul", "m", "n"; "m" !Zero (.\ "m"; !Add "n" ("Mul" "m" "n"))).


Lemma Mul_rec_0 m :
  Mul Zero (enc m) == Zero.

Lemma Mul_rec_S n m :
  Mul (enc (S n)) (enc m) == (Add (enc m)) (((lam (Mul #0)) (enc n)) (enc m)).

Lemma Mul_correct m n :
  Mul (enc n) (enc m) == enc (n × m).