include "basic_1/tlist/fwd.ma".
-theorem pr3_iso_appls_abbr:
+lemma pr3_iso_appls_abbr:
\forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c
(CHead d (Bind Abbr) w)) \to (\forall (vs: TList).(let u1 \def (THeads (Flat
Appl) vs (TLRef i)) in (\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to
Appl) (lift (S O) O x4) x3) (pr3_thin_dx (CHead c (Bind x0) x5) x2 x3 H10
(lift (S O) O x4) Appl)) u2 H7)))))))))))))) H4)) H3)))))))) vs)))))).
-theorem pr3_iso_appls_cast:
+lemma pr3_iso_appls_cast:
\forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (vs: TList).(let u1
\def (THeads (Flat Appl) vs (THead (Flat Cast) v t)) in (\forall (u2:
T).((pr3 c u1 u2) \to ((((iso u1 u2) \to (\forall (P: Prop).P))) \to (pr3 c
(THead (Flat Appl) (lift (S O) O x4) x3) (pr3_thin_dx (CHead c (Bind x0) x5)
x2 x3 H9 (lift (S O) O x4) Appl)) u2 H6)))))))))))))) H3)) H2)))))))) vs)))).
-theorem pr3_iso_appl_bind:
+lemma pr3_iso_appl_bind:
\forall (b: B).((not (eq B b Abst)) \to (\forall (v1: T).(\forall (v2:
T).(\forall (t: T).(let u1 \def (THead (Flat Appl) v1 (THead (Bind b) v2 t))
in (\forall (c: C).(\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to
(Bind x0) x1 x2))) (lift_flat Appl x4 (THead (Bind x0) x1 x2) (S O) O))))
H10))) u2 H6))))))))))))) H3)) H2)))))))))).
-theorem pr3_iso_appls_appl_bind:
+lemma pr3_iso_appls_appl_bind:
\forall (b: B).((not (eq B b Abst)) \to (\forall (v: T).(\forall (u:
T).(\forall (t: T).(\forall (vs: TList).(let u1 \def (THeads (Flat Appl) vs
(THead (Flat Appl) v (THead (Bind b) u t))) in (\forall (c: C).(\forall (u2:
(pr3_thin_dx (CHead c (Bind x0) x5) x2 x3 H10 (lift (S O) O x4) Appl)) u2
H7)))))))))))))) H4)) H3))))))))) vs)))))).
-theorem pr3_iso_appls_bind:
+lemma pr3_iso_appls_bind:
\forall (b: B).((not (eq B b Abst)) \to (\forall (vs: TList).(\forall (u:
T).(\forall (t: T).(let u1 \def (THeads (Flat Appl) vs (THead (Bind b) u t))
in (\forall (c: C).(\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to
Appl) (lift (S O) O t) t0 (lifts (S O) O ts))) (lifts (S O) O (TApp ts t))
(lifts_tapp (S O) O t ts))))))))))) vs))).
-theorem pr3_iso_beta:
+lemma pr3_iso_beta:
\forall (v: T).(\forall (w: T).(\forall (t: T).(let u1 \def (THead (Flat
Appl) v (THead (Bind Abst) w t)) in (\forall (c: C).(\forall (u2: T).((pr3 c
u1 u2) \to ((((iso u1 u2) \to (\forall (P: Prop).P))) \to (pr3 c (THead (Bind
False with []) in H23))))))))) H14)) H13))))))) H9)))))))))))))) H2))
H1)))))))).
-theorem pr3_iso_appls_beta:
+lemma pr3_iso_appls_beta:
\forall (us: TList).(\forall (v: T).(\forall (w: T).(\forall (t: T).(let u1
\def (THeads (Flat Appl) us (THead (Flat Appl) v (THead (Bind Abst) w t))) in
(\forall (c: C).(\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to