# Size of terms

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

# Properties of the encoding for nat

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

Fixpoint unenc (s : term) :=
match s with
| lam (lam #1) ⇒ Some 0
| lam (lam (app #0 s)) ⇒ match unenc s with Some nSome (S n) | xx end
| _None
end.

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

Lemma unenc_correct2 t n : unenc t = Some nenc n = t.

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

# Encoding for terms

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 ts = t.

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

# Interalized encoding combinators

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).

# Interalized encoding of natural numbers

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).

# Interalized term encoding

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).