Library EnumInt

Definition AppCross := R (.\"aC", "A", "B";
  "A" !Nil (.\"a", "A"; !Append ("aC" "A" "B") (!Map (.\"x"; !App "a" "x") "B"))).


Definition tlenc := @lenc term tenc.

Lemma tlenc_lam B : lambda (tlenc B).

Lemma tlenc_cls B : closed (tlenc B).



Lemma AppCross_Nil B : AppCross Nil (tlenc B) == Nil.

Lemma AppCross_Cons a A B : AppCross (tlenc (a::A)) (tlenc B) == Append ((lam (AppCross #0)) (tlenc A) (tlenc B)) (Map (lam (App (tenc a) #0)) (tlenc B)).

Lemma AppCross_correct A B : AppCross (tlenc A) (tlenc B) == tlenc(appCross A B).

Definition Exh_size := R (.\ "Es", "s";
  "s" !I (.\ "s", "t"; !Add (!Add !(enc 1) ("Es" "s")) ("Es" "t")) (.\ "s"; (!Succ ("Es" "s")))).


Lemma Exh_size_var n : Exh_size (tenc #n) == enc n.

Lemma Exh_size_app (s t : term) : Exh_size (tenc (s t))
   == Add (Add (enc 1) ((lam (Exh_size #0)) (tenc s))) ((lam (Exh_size #0)) (tenc t)).

Lemma Exh_size_lam s : Exh_size (tenc (lam s)) == Succ ((lam(Exh_size #0)) (tenc s)).

Lemma Exh_size_correct s : Exh_size (tenc s) == enc(exh_size s).

Definition TT := R (.\ "TT", "n";
  "n" !(tlenc([#0]))
      (.\"n"; (!Append
              (!Append ("TT" "n") (!Cons (!Var (!Succ "n")) !Nil))
             (!Filter (.\"x"; (!Not (!(El Eq) "x" ("TT" "n"))))
               (!Append (!Map !Lam ("TT" "n"))
                       (!AppCross ("TT" "n") ("TT" "n"))
               )))
     )
).

Lemma TT_0 : TT (enc 0) == tlenc([#0]).

Lemma TT_S n : TT (enc (S n)) == Append (Append ((lam(TT #0)) (enc n)) (Cons (Var (Succ (enc n))) Nil)) (Filter (lam(Not (El Eq #0 ((lam(TT #0)) (enc n))))) (Append (Map Lam ((lam(TT #0)) (enc n))) (AppCross ((lam(TT #0)) (enc n)) ((lam(TT #0)) (enc n))))).

Lemma TT_correct n : TT (enc n) == tlenc(T n).

Definition U : term := .\"n";
  (!Nth (!TT "n") "n") !I !(tenc #0).


Lemma U_correct n : U (enc n) == tenc(g_inv n).