Fixpoint size (t : term) :=
  match t with
  | var n ⇒ 1
  | app s t ⇒ size s + size t
  | lam s ⇒ 1 + size s
  end.

Lemma enc_injective m n : enc m = enc n → m = n.

Fixpoint unenc (s : term) :=
match s with
| lam (lam #1) ⇒ Some 0
| lam (lam (app #0 s)) ⇒ match unenc s with Some n ⇒ Some (S n) | x⇒x end
| _ ⇒ None
end.

Lemma unenc_correct m : (unenc (enc m)) = Some m.

Lemma unenc_correct2 t n : unenc t = Some n → enc n = t.

Lemma dec_enc t : dec (∃ n, t = enc n).

Fixpoint tenc (t : term) :=
  lam ( lam ( lam (
     match t with
       | var n ⇒ (var 2) (enc n)
       | app s t ⇒ (var 1) (tenc s) (tenc t)
       | lam s ⇒ (var 0) (tenc s)
     end
  ))).

Lemma tenc_cls s : closed (tenc s).

Lemma tenc_lam s : lambda (tenc s).


Lemma tenc_injective s t : tenc s = tenc t → s = t.

Lemma tenc_inj s t : tenc s == tenc t → s = t.

Definition Var : term := .\"n"; .\"v","a","l"; "v" "n".
Definition App : term := .\"s","t"; .\"v","a","l"; "a" "s" "t".
Definition Lam : term := .\"s"; .\"v","a","l"; "l" "s".



Lemma App_correct s t : App (tenc s) (tenc t) == tenc (s t).

Lemma Lam_correct s : Lam (tenc s) == tenc (lam s).

Lemma Var_correct n : Var (enc n) == tenc (#n).

Definition P := R( .\"P", "n"; "n" !(tenc Zero) (.\"n"; !Lam (!Lam (!App !(tenc 0) ("P" "n"))))).


Lemma P_correct n : P (enc n) == tenc(enc n).

Definition Q := R( .\"Q", "s"; "s" (.\"n"; !Lam (!Lam (!Lam (!App !(tenc 2) (!P "n")))))
                                   (.\"s","t"; !Lam (!Lam (!Lam (!App (!App !(tenc 1) ("Q" "s")) ("Q" "t")))))
                                   (.\"s"; !Lam (!Lam (!Lam (!App !(tenc 0) ("Q" "s"))))) ).

Lemma Q_rec_var n : Q (tenc (# n)) == Lam (Lam (Lam (App (tenc #2) (P (enc n))))).

Lemma Q_rec_app s t : Q (tenc (app s t)) == Lam (Lam (Lam (App (App (tenc #1) (Q (tenc s))) (Q (tenc t))))).

Lemma Q_rec_lam s : Q (tenc (lam s)) == Lam (Lam (Lam (App (tenc #0) (Q (tenc s))))).

Lemma Q_correct s : Q (tenc s) == tenc(tenc s).