include "basic_1/pr2/fwd.ma".
-theorem nf2_sort:
+lemma nf2_sort:
\forall (c: C).(\forall (n: nat).(nf2 c (TSort n)))
\def
\lambda (c: C).(\lambda (n: nat).(\lambda (t2: T).(\lambda (H: (pr2 c (TSort
-n) t2)).(let TMP_1 \def (TSort n) in (let TMP_3 \def (\lambda (t: T).(let
-TMP_2 \def (TSort n) in (eq T TMP_2 t))) in (let TMP_4 \def (TSort n) in (let
-TMP_5 \def (refl_equal T TMP_4) in (let TMP_6 \def (pr2_gen_sort c t2 n H) in
-(eq_ind_r T TMP_1 TMP_3 TMP_5 t2 TMP_6))))))))).
+n) t2)).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (TSort n) t)) (refl_equal
+T (TSort n)) t2 (pr2_gen_sort c t2 n H))))).
-theorem nf2_csort_lref:
+lemma nf2_csort_lref:
\forall (n: nat).(\forall (i: nat).(nf2 (CSort n) (TLRef i)))
\def
\lambda (n: nat).(\lambda (i: nat).(\lambda (t2: T).(\lambda (H: (pr2 (CSort
-n) (TLRef i) t2)).(let TMP_1 \def (CSort n) in (let H0 \def (pr2_gen_lref
-TMP_1 t2 i H) in (let TMP_2 \def (TLRef i) in (let TMP_3 \def (eq T t2 TMP_2)
-in (let TMP_7 \def (\lambda (d: C).(\lambda (u: T).(let TMP_4 \def (CSort n)
-in (let TMP_5 \def (Bind Abbr) in (let TMP_6 \def (CHead d TMP_5 u) in (getl
-i TMP_4 TMP_6)))))) in (let TMP_10 \def (\lambda (_: C).(\lambda (u: T).(let
-TMP_8 \def (S i) in (let TMP_9 \def (lift TMP_8 O u) in (eq T t2 TMP_9)))))
-in (let TMP_11 \def (ex2_2 C T TMP_7 TMP_10) in (let TMP_12 \def (TLRef i) in
-(let TMP_13 \def (eq T TMP_12 t2) in (let TMP_19 \def (\lambda (H1: (eq T t2
-(TLRef i))).(let TMP_14 \def (TLRef i) in (let TMP_16 \def (\lambda (t:
-T).(let TMP_15 \def (TLRef i) in (eq T TMP_15 t))) in (let TMP_17 \def (TLRef
-i) in (let TMP_18 \def (refl_equal T TMP_17) in (eq_ind_r T TMP_14 TMP_16
-TMP_18 t2 H1)))))) in (let TMP_41 \def (\lambda (H1: (ex2_2 C T (\lambda (d:
-C).(\lambda (u: T).(getl i (CSort n) (CHead d (Bind Abbr) u)))) (\lambda (_:
-C).(\lambda (u: T).(eq T t2 (lift (S i) O u)))))).(let TMP_23 \def (\lambda
-(d: C).(\lambda (u: T).(let TMP_20 \def (CSort n) in (let TMP_21 \def (Bind
-Abbr) in (let TMP_22 \def (CHead d TMP_21 u) in (getl i TMP_20 TMP_22))))))
-in (let TMP_26 \def (\lambda (_: C).(\lambda (u: T).(let TMP_24 \def (S i) in
-(let TMP_25 \def (lift TMP_24 O u) in (eq T t2 TMP_25))))) in (let TMP_27
-\def (TLRef i) in (let TMP_28 \def (eq T TMP_27 t2) in (let TMP_40 \def
-(\lambda (x0: C).(\lambda (x1: T).(\lambda (H2: (getl i (CSort n) (CHead x0
-(Bind Abbr) x1))).(\lambda (H3: (eq T t2 (lift (S i) O x1))).(let TMP_29 \def
-(S i) in (let TMP_30 \def (lift TMP_29 O x1) in (let TMP_32 \def (\lambda (t:
-T).(let TMP_31 \def (TLRef i) in (eq T TMP_31 t))) in (let TMP_33 \def (Bind
-Abbr) in (let TMP_34 \def (CHead x0 TMP_33 x1) in (let TMP_35 \def (TLRef i)
-in (let TMP_36 \def (S i) in (let TMP_37 \def (lift TMP_36 O x1) in (let
-TMP_38 \def (eq T TMP_35 TMP_37) in (let TMP_39 \def (getl_gen_sort n i
-TMP_34 H2 TMP_38) in (eq_ind_r T TMP_30 TMP_32 TMP_39 t2 H3))))))))))))))) in
-(ex2_2_ind C T TMP_23 TMP_26 TMP_28 TMP_40 H1))))))) in (or_ind TMP_3 TMP_11
-TMP_13 TMP_19 TMP_41 H0))))))))))))))).
+n) (TLRef i) t2)).(let H0 \def (pr2_gen_lref (CSort n) t2 i H) in (or_ind (eq
+T t2 (TLRef i)) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i (CSort n)
+(CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift (S
+i) O u))))) (eq T (TLRef i) t2) (\lambda (H1: (eq T t2 (TLRef i))).(eq_ind_r
+T (TLRef i) (\lambda (t: T).(eq T (TLRef i) t)) (refl_equal T (TLRef i)) t2
+H1)) (\lambda (H1: (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i (CSort
+n) (CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift
+(S i) O u)))))).(ex2_2_ind C T (\lambda (d: C).(\lambda (u: T).(getl i (CSort
+n) (CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift
+(S i) O u)))) (eq T (TLRef i) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda
+(H2: (getl i (CSort n) (CHead x0 (Bind Abbr) x1))).(\lambda (H3: (eq T t2
+(lift (S i) O x1))).(eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(eq T
+(TLRef i) t)) (getl_gen_sort n i (CHead x0 (Bind Abbr) x1) H2 (eq T (TLRef i)
+(lift (S i) O x1))) t2 H3))))) H1)) H0))))).
theorem nf2_abst:
\forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (b: B).(\forall (v:
\to (eq T u t2))))).(\lambda (b: B).(\lambda (v: T).(\lambda (t: T).(\lambda
(H0: ((\forall (t2: T).((pr2 (CHead c (Bind b) v) t t2) \to (eq T t
t2))))).(\lambda (t2: T).(\lambda (H1: (pr2 c (THead (Bind Abst) u t)
-t2)).(let H2 \def (pr2_gen_abst c u t t2 H1) in (let TMP_3 \def (\lambda (u2:
-T).(\lambda (t3: T).(let TMP_1 \def (Bind Abst) in (let TMP_2 \def (THead
-TMP_1 u2 t3) in (eq T t2 TMP_2))))) in (let TMP_4 \def (\lambda (u2:
-T).(\lambda (_: T).(pr2 c u u2))) in (let TMP_7 \def (\lambda (_: T).(\lambda
-(t3: T).(\forall (b0: B).(\forall (u0: T).(let TMP_5 \def (Bind b0) in (let
-TMP_6 \def (CHead c TMP_5 u0) in (pr2 TMP_6 t t3))))))) in (let TMP_8 \def
-(Bind Abst) in (let TMP_9 \def (THead TMP_8 u t) in (let TMP_10 \def (eq T
-TMP_9 t2) in (let TMP_24 \def (\lambda (x0: T).(\lambda (x1: T).(\lambda (H3:
-(eq T t2 (THead (Bind Abst) x0 x1))).(\lambda (H4: (pr2 c u x0)).(\lambda
-(H5: ((\forall (b0: B).(\forall (u0: T).(pr2 (CHead c (Bind b0) u0) t
-x1))))).(let TMP_11 \def (Bind Abst) in (let TMP_12 \def (THead TMP_11 x0 x1)
-in (let TMP_15 \def (\lambda (t0: T).(let TMP_13 \def (Bind Abst) in (let
-TMP_14 \def (THead TMP_13 u t) in (eq T TMP_14 t0)))) in (let TMP_16 \def
-(Bind Abst) in (let TMP_17 \def (Bind Abst) in (let TMP_18 \def (Bind Abst)
-in (let TMP_19 \def (refl_equal K TMP_18) in (let TMP_20 \def (H x0 H4) in
-(let TMP_21 \def (H5 b v) in (let TMP_22 \def (H0 x1 TMP_21) in (let TMP_23
-\def (f_equal3 K T T T THead TMP_16 TMP_17 u x0 t x1 TMP_19 TMP_20 TMP_22) in
-(eq_ind_r T TMP_12 TMP_15 TMP_23 t2 H3))))))))))))))))) in (ex3_2_ind T T
-TMP_3 TMP_4 TMP_7 TMP_10 TMP_24 H2))))))))))))))))).
+t2)).(let H2 \def (pr2_gen_abst c u t t2 H1) in (ex3_2_ind T T (\lambda (u2:
+T).(\lambda (t3: T).(eq T t2 (THead (Bind Abst) u2 t3)))) (\lambda (u2:
+T).(\lambda (_: T).(pr2 c u u2))) (\lambda (_: T).(\lambda (t3: T).(\forall
+(b0: B).(\forall (u0: T).(pr2 (CHead c (Bind b0) u0) t t3))))) (eq T (THead
+(Bind Abst) u t) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H3: (eq T t2
+(THead (Bind Abst) x0 x1))).(\lambda (H4: (pr2 c u x0)).(\lambda (H5:
+((\forall (b0: B).(\forall (u0: T).(pr2 (CHead c (Bind b0) u0) t
+x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T (THead
+(Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst) u x0 t
+x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 b v))) t2 H3))))))
+H2)))))))))).
theorem nf2_abst_shift:
\forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (t: T).((nf2 (CHead c
\to (eq T u t2))))).(\lambda (t: T).(\lambda (H0: ((\forall (t2: T).((pr2
(CHead c (Bind Abst) u) t t2) \to (eq T t t2))))).(\lambda (t2: T).(\lambda
(H1: (pr2 c (THead (Bind Abst) u t) t2)).(let H2 \def (pr2_gen_abst c u t t2
-H1) in (let TMP_3 \def (\lambda (u2: T).(\lambda (t3: T).(let TMP_1 \def
-(Bind Abst) in (let TMP_2 \def (THead TMP_1 u2 t3) in (eq T t2 TMP_2))))) in
-(let TMP_4 \def (\lambda (u2: T).(\lambda (_: T).(pr2 c u u2))) in (let TMP_7
-\def (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(let
-TMP_5 \def (Bind b) in (let TMP_6 \def (CHead c TMP_5 u0) in (pr2 TMP_6 t
-t3))))))) in (let TMP_8 \def (Bind Abst) in (let TMP_9 \def (THead TMP_8 u t)
-in (let TMP_10 \def (eq T TMP_9 t2) in (let TMP_24 \def (\lambda (x0:
-T).(\lambda (x1: T).(\lambda (H3: (eq T t2 (THead (Bind Abst) x0
-x1))).(\lambda (H4: (pr2 c u x0)).(\lambda (H5: ((\forall (b: B).(\forall
-(u0: T).(pr2 (CHead c (Bind b) u0) t x1))))).(let TMP_11 \def (Bind Abst) in
-(let TMP_12 \def (THead TMP_11 x0 x1) in (let TMP_15 \def (\lambda (t0:
-T).(let TMP_13 \def (Bind Abst) in (let TMP_14 \def (THead TMP_13 u t) in (eq
-T TMP_14 t0)))) in (let TMP_16 \def (Bind Abst) in (let TMP_17 \def (Bind
-Abst) in (let TMP_18 \def (Bind Abst) in (let TMP_19 \def (refl_equal K
-TMP_18) in (let TMP_20 \def (H x0 H4) in (let TMP_21 \def (H5 Abst u) in (let
-TMP_22 \def (H0 x1 TMP_21) in (let TMP_23 \def (f_equal3 K T T T THead TMP_16
-TMP_17 u x0 t x1 TMP_19 TMP_20 TMP_22) in (eq_ind_r T TMP_12 TMP_15 TMP_23 t2
-H3))))))))))))))))) in (ex3_2_ind T T TMP_3 TMP_4 TMP_7 TMP_10 TMP_24
-H2))))))))))))))).
+H1) in (ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
+Abst) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c u u2))) (\lambda (_:
+T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b)
+u0) t t3))))) (eq T (THead (Bind Abst) u t) t2) (\lambda (x0: T).(\lambda
+(x1: T).(\lambda (H3: (eq T t2 (THead (Bind Abst) x0 x1))).(\lambda (H4: (pr2
+c u x0)).(\lambda (H5: ((\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind
+b) u0) t x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T
+(THead (Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst)
+u x0 t x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 Abst u))) t2
+H3)))))) H2)))))))).
-theorem nfs2_tapp:
+lemma nfs2_tapp:
\forall (c: C).(\forall (t: T).(\forall (ts: TList).((nfs2 c (TApp ts t))
\to (land (nfs2 c ts) (nf2 c t)))))
\def
- \lambda (c: C).(\lambda (t: T).(\lambda (ts: TList).(let TMP_3 \def (\lambda
-(t0: TList).((nfs2 c (TApp t0 t)) \to (let TMP_1 \def (nfs2 c t0) in (let
-TMP_2 \def (nf2 c t) in (land TMP_1 TMP_2))))) in (let TMP_9 \def (\lambda
-(H: (land (nf2 c t) True)).(let H0 \def H in (let TMP_4 \def (nf2 c t) in
-(let TMP_5 \def (nf2 c t) in (let TMP_6 \def (land True TMP_5) in (let TMP_8
-\def (\lambda (H1: (nf2 c t)).(\lambda (_: True).(let TMP_7 \def (nf2 c t) in
-(conj True TMP_7 I H1)))) in (land_ind TMP_4 True TMP_6 TMP_8 H0))))))) in
-(let TMP_34 \def (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H: (((nfs2 c
+ \lambda (c: C).(\lambda (t: T).(\lambda (ts: TList).(TList_ind (\lambda (t0:
+TList).((nfs2 c (TApp t0 t)) \to (land (nfs2 c t0) (nf2 c t)))) (\lambda (H:
+(land (nf2 c t) True)).(let H0 \def H in (land_ind (nf2 c t) True (land True
+(nf2 c t)) (\lambda (H1: (nf2 c t)).(\lambda (_: True).(conj True (nf2 c t) I
+H1))) H0))) (\lambda (t0: T).(\lambda (t1: TList).(\lambda (H: (((nfs2 c
(TApp t1 t)) \to (land (nfs2 c t1) (nf2 c t))))).(\lambda (H0: (land (nf2 c
-t0) (nfs2 c (TApp t1 t)))).(let H1 \def H0 in (let TMP_10 \def (nf2 c t0) in
-(let TMP_11 \def (TApp t1 t) in (let TMP_12 \def (nfs2 c TMP_11) in (let
-TMP_13 \def (nf2 c t0) in (let TMP_14 \def (nfs2 c t1) in (let TMP_15 \def
-(land TMP_13 TMP_14) in (let TMP_16 \def (nf2 c t) in (let TMP_17 \def (land
-TMP_15 TMP_16) in (let TMP_33 \def (\lambda (H2: (nf2 c t0)).(\lambda (H3:
-(nfs2 c (TApp t1 t))).(let H_x \def (H H3) in (let H4 \def H_x in (let TMP_18
-\def (nfs2 c t1) in (let TMP_19 \def (nf2 c t) in (let TMP_20 \def (nf2 c t0)
-in (let TMP_21 \def (nfs2 c t1) in (let TMP_22 \def (land TMP_20 TMP_21) in
-(let TMP_23 \def (nf2 c t) in (let TMP_24 \def (land TMP_22 TMP_23) in (let
-TMP_32 \def (\lambda (H5: (nfs2 c t1)).(\lambda (H6: (nf2 c t)).(let TMP_25
-\def (nf2 c t0) in (let TMP_26 \def (nfs2 c t1) in (let TMP_27 \def (land
-TMP_25 TMP_26) in (let TMP_28 \def (nf2 c t) in (let TMP_29 \def (nf2 c t0)
-in (let TMP_30 \def (nfs2 c t1) in (let TMP_31 \def (conj TMP_29 TMP_30 H2
-H5) in (conj TMP_27 TMP_28 TMP_31 H6)))))))))) in (land_ind TMP_18 TMP_19
-TMP_24 TMP_32 H4))))))))))))) in (land_ind TMP_10 TMP_12 TMP_17 TMP_33
-H1))))))))))))))) in (TList_ind TMP_3 TMP_9 TMP_34 ts)))))).
+t0) (nfs2 c (TApp t1 t)))).(let H1 \def H0 in (land_ind (nf2 c t0) (nfs2 c
+(TApp t1 t)) (land (land (nf2 c t0) (nfs2 c t1)) (nf2 c t)) (\lambda (H2:
+(nf2 c t0)).(\lambda (H3: (nfs2 c (TApp t1 t))).(let H_x \def (H H3) in (let
+H4 \def H_x in (land_ind (nfs2 c t1) (nf2 c t) (land (land (nf2 c t0) (nfs2 c
+t1)) (nf2 c t)) (\lambda (H5: (nfs2 c t1)).(\lambda (H6: (nf2 c t)).(conj
+(land (nf2 c t0) (nfs2 c t1)) (nf2 c t) (conj (nf2 c t0) (nfs2 c t1) H2 H5)
+H6))) H4))))) H1)))))) ts))).
-theorem nf2_appls_lref:
+lemma nf2_appls_lref:
\forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (vs:
TList).((nfs2 c vs) \to (nf2 c (THeads (Flat Appl) vs (TLRef i)))))))
\def
\lambda (c: C).(\lambda (i: nat).(\lambda (H: (nf2 c (TLRef i))).(\lambda
-(vs: TList).(let TMP_4 \def (\lambda (t: TList).((nfs2 c t) \to (let TMP_1
-\def (Flat Appl) in (let TMP_2 \def (TLRef i) in (let TMP_3 \def (THeads
-TMP_1 t TMP_2) in (nf2 c TMP_3)))))) in (let TMP_5 \def (\lambda (_: True).H)
-in (let TMP_295 \def (\lambda (t: T).(\lambda (t0: TList).(\lambda (H0:
-(((nfs2 c t0) \to (nf2 c (THeads (Flat Appl) t0 (TLRef i)))))).(\lambda (H1:
-(land (nf2 c t) (nfs2 c t0))).(let H2 \def H1 in (let TMP_6 \def (nf2 c t) in
-(let TMP_7 \def (nfs2 c t0) in (let TMP_8 \def (Flat Appl) in (let TMP_9 \def
-(Flat Appl) in (let TMP_10 \def (TLRef i) in (let TMP_11 \def (THeads TMP_9
-t0 TMP_10) in (let TMP_12 \def (THead TMP_8 t TMP_11) in (let TMP_13 \def
-(nf2 c TMP_12) in (let TMP_294 \def (\lambda (H3: (nf2 c t)).(\lambda (H4:
-(nfs2 c t0)).(let H_y \def (H0 H4) in (\lambda (t2: T).(\lambda (H5: (pr2 c
-(THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2)).(let TMP_14 \def
-(Flat Appl) in (let TMP_15 \def (TLRef i) in (let TMP_16 \def (THeads TMP_14
-t0 TMP_15) in (let H6 \def (pr2_gen_appl c t TMP_16 t2 H5) in (let TMP_19
-\def (\lambda (u2: T).(\lambda (t3: T).(let TMP_17 \def (Flat Appl) in (let
-TMP_18 \def (THead TMP_17 u2 t3) in (eq T t2 TMP_18))))) in (let TMP_20 \def
-(\lambda (u2: T).(\lambda (_: T).(pr2 c t u2))) in (let TMP_24 \def (\lambda
-(_: T).(\lambda (t3: T).(let TMP_21 \def (Flat Appl) in (let TMP_22 \def
-(TLRef i) in (let TMP_23 \def (THeads TMP_21 t0 TMP_22) in (pr2 c TMP_23
-t3)))))) in (let TMP_25 \def (ex3_2 T T TMP_19 TMP_20 TMP_24) in (let TMP_31
-\def (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(let
-TMP_26 \def (Flat Appl) in (let TMP_27 \def (TLRef i) in (let TMP_28 \def
-(THeads TMP_26 t0 TMP_27) in (let TMP_29 \def (Bind Abst) in (let TMP_30 \def
-(THead TMP_29 y1 z1) in (eq T TMP_28 TMP_30)))))))))) in (let TMP_34 \def
-(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(let TMP_32
-\def (Bind Abbr) in (let TMP_33 \def (THead TMP_32 u2 t3) in (eq T t2
-TMP_33))))))) in (let TMP_35 \def (\lambda (_: T).(\lambda (_: T).(\lambda
-(u2: T).(\lambda (_: T).(pr2 c t u2))))) in (let TMP_38 \def (\lambda (_:
-T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall
-(u: T).(let TMP_36 \def (Bind b) in (let TMP_37 \def (CHead c TMP_36 u) in
-(pr2 TMP_37 z1 t3))))))))) in (let TMP_39 \def (ex4_4 T T T T TMP_31 TMP_34
-TMP_35 TMP_38) in (let TMP_41 \def (\lambda (b: B).(\lambda (_: T).(\lambda
-(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(let TMP_40 \def (eq B
-b Abst) in (not TMP_40)))))))) in (let TMP_47 \def (\lambda (b: B).(\lambda
-(y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(let
-TMP_42 \def (Flat Appl) in (let TMP_43 \def (TLRef i) in (let TMP_44 \def
-(THeads TMP_42 t0 TMP_43) in (let TMP_45 \def (Bind b) in (let TMP_46 \def
-(THead TMP_45 y1 z1) in (eq T TMP_44 TMP_46)))))))))))) in (let TMP_54 \def
-(\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda
-(u2: T).(\lambda (y2: T).(let TMP_48 \def (Bind b) in (let TMP_49 \def (Flat
-Appl) in (let TMP_50 \def (S O) in (let TMP_51 \def (lift TMP_50 O u2) in
-(let TMP_52 \def (THead TMP_49 TMP_51 z2) in (let TMP_53 \def (THead TMP_48
-y2 TMP_52) in (eq T t2 TMP_53))))))))))))) in (let TMP_55 \def (\lambda (_:
-B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
-(_: T).(pr2 c t u2))))))) in (let TMP_56 \def (\lambda (_: B).(\lambda (y1:
-T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
-y2))))))) in (let TMP_59 \def (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
-T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(let TMP_57 \def (Bind
-b) in (let TMP_58 \def (CHead c TMP_57 y2) in (pr2 TMP_58 z1 z2))))))))) in
-(let TMP_60 \def (ex6_6 B T T T T T TMP_41 TMP_47 TMP_54 TMP_55 TMP_56
-TMP_59) in (let TMP_61 \def (Flat Appl) in (let TMP_62 \def (Flat Appl) in
-(let TMP_63 \def (TLRef i) in (let TMP_64 \def (THeads TMP_62 t0 TMP_63) in
-(let TMP_65 \def (THead TMP_61 t TMP_64) in (let TMP_66 \def (eq T TMP_65 t2)
-in (let TMP_132 \def (\lambda (H7: (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
-T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_:
-T).(pr2 c t u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c (THeads (Flat Appl)
-t0 (TLRef i)) t3))))).(let TMP_69 \def (\lambda (u2: T).(\lambda (t3: T).(let
-TMP_67 \def (Flat Appl) in (let TMP_68 \def (THead TMP_67 u2 t3) in (eq T t2
-TMP_68))))) in (let TMP_70 \def (\lambda (u2: T).(\lambda (_: T).(pr2 c t
-u2))) in (let TMP_74 \def (\lambda (_: T).(\lambda (t3: T).(let TMP_71 \def
-(Flat Appl) in (let TMP_72 \def (TLRef i) in (let TMP_73 \def (THeads TMP_71
-t0 TMP_72) in (pr2 c TMP_73 t3)))))) in (let TMP_75 \def (Flat Appl) in (let
-TMP_76 \def (Flat Appl) in (let TMP_77 \def (TLRef i) in (let TMP_78 \def
-(THeads TMP_76 t0 TMP_77) in (let TMP_79 \def (THead TMP_75 t TMP_78) in (let
-TMP_80 \def (eq T TMP_79 t2) in (let TMP_131 \def (\lambda (x0: T).(\lambda
-(x1: T).(\lambda (H8: (eq T t2 (THead (Flat Appl) x0 x1))).(\lambda (H9: (pr2
-c t x0)).(\lambda (H10: (pr2 c (THeads (Flat Appl) t0 (TLRef i)) x1)).(let
-TMP_81 \def (Flat Appl) in (let TMP_82 \def (THead TMP_81 x0 x1) in (let
-TMP_88 \def (\lambda (t1: T).(let TMP_83 \def (Flat Appl) in (let TMP_84 \def
-(Flat Appl) in (let TMP_85 \def (TLRef i) in (let TMP_86 \def (THeads TMP_84
-t0 TMP_85) in (let TMP_87 \def (THead TMP_83 t TMP_86) in (eq T TMP_87
-t1))))))) in (let TMP_92 \def (\lambda (t1: T).(let TMP_89 \def (Flat Appl)
-in (let TMP_90 \def (TLRef i) in (let TMP_91 \def (THeads TMP_89 t0 TMP_90)
-in (pr2 c TMP_91 t1))))) in (let TMP_93 \def (Flat Appl) in (let TMP_94 \def
-(TLRef i) in (let TMP_95 \def (THeads TMP_93 t0 TMP_94) in (let TMP_96 \def
-(H_y x1 H10) in (let H11 \def (eq_ind_r T x1 TMP_92 H10 TMP_95 TMP_96) in
-(let TMP_97 \def (Flat Appl) in (let TMP_98 \def (TLRef i) in (let TMP_99
-\def (THeads TMP_97 t0 TMP_98) in (let TMP_107 \def (\lambda (t1: T).(let
-TMP_100 \def (Flat Appl) in (let TMP_101 \def (Flat Appl) in (let TMP_102
-\def (TLRef i) in (let TMP_103 \def (THeads TMP_101 t0 TMP_102) in (let
-TMP_104 \def (THead TMP_100 t TMP_103) in (let TMP_105 \def (Flat Appl) in
-(let TMP_106 \def (THead TMP_105 x0 t1) in (eq T TMP_104 TMP_106))))))))) in
-(let TMP_108 \def (\lambda (t1: T).(pr2 c t t1)) in (let TMP_109 \def (H3 x0
-H9) in (let H12 \def (eq_ind_r T x0 TMP_108 H9 t TMP_109) in (let TMP_120
-\def (\lambda (t1: T).(let TMP_110 \def (Flat Appl) in (let TMP_111 \def
-(Flat Appl) in (let TMP_112 \def (TLRef i) in (let TMP_113 \def (THeads
-TMP_111 t0 TMP_112) in (let TMP_114 \def (THead TMP_110 t TMP_113) in (let
-TMP_115 \def (Flat Appl) in (let TMP_116 \def (Flat Appl) in (let TMP_117
-\def (TLRef i) in (let TMP_118 \def (THeads TMP_116 t0 TMP_117) in (let
-TMP_119 \def (THead TMP_115 t1 TMP_118) in (eq T TMP_114 TMP_119))))))))))))
-in (let TMP_121 \def (Flat Appl) in (let TMP_122 \def (Flat Appl) in (let
-TMP_123 \def (TLRef i) in (let TMP_124 \def (THeads TMP_122 t0 TMP_123) in
-(let TMP_125 \def (THead TMP_121 t TMP_124) in (let TMP_126 \def (refl_equal
-T TMP_125) in (let TMP_127 \def (H3 x0 H9) in (let TMP_128 \def (eq_ind T t
-TMP_120 TMP_126 x0 TMP_127) in (let TMP_129 \def (H_y x1 H10) in (let TMP_130
-\def (eq_ind T TMP_99 TMP_107 TMP_128 x1 TMP_129) in (eq_ind_r T TMP_82
-TMP_88 TMP_130 t2 H8))))))))))))))))))))))))))))))))) in (ex3_2_ind T T
-TMP_69 TMP_70 TMP_74 TMP_80 TMP_131 H7)))))))))))) in (let TMP_201 \def
-(\lambda (H7: (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
-T).(\lambda (_: T).(eq T (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst)
-y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3:
-T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
-T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t u2))))) (\lambda (_: T).(\lambda
-(z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2
-(CHead c (Bind b) u) z1 t3))))))))).(let TMP_138 \def (\lambda (y1:
-T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(let TMP_133 \def (Flat
-Appl) in (let TMP_134 \def (TLRef i) in (let TMP_135 \def (THeads TMP_133 t0
-TMP_134) in (let TMP_136 \def (Bind Abst) in (let TMP_137 \def (THead TMP_136
-y1 z1) in (eq T TMP_135 TMP_137)))))))))) in (let TMP_141 \def (\lambda (_:
-T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(let TMP_139 \def (Bind
-Abbr) in (let TMP_140 \def (THead TMP_139 u2 t3) in (eq T t2 TMP_140)))))))
-in (let TMP_142 \def (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
-T).(\lambda (_: T).(pr2 c t u2))))) in (let TMP_145 \def (\lambda (_:
-T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall
-(u: T).(let TMP_143 \def (Bind b) in (let TMP_144 \def (CHead c TMP_143 u) in
-(pr2 TMP_144 z1 t3))))))))) in (let TMP_146 \def (Flat Appl) in (let TMP_147
-\def (Flat Appl) in (let TMP_148 \def (TLRef i) in (let TMP_149 \def (THeads
-TMP_147 t0 TMP_148) in (let TMP_150 \def (THead TMP_146 t TMP_149) in (let
-TMP_151 \def (eq T TMP_150 t2) in (let TMP_200 \def (\lambda (x0: T).(\lambda
-(x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (H8: (eq T (THeads (Flat
-Appl) t0 (TLRef i)) (THead (Bind Abst) x0 x1))).(\lambda (H9: (eq T t2 (THead
-(Bind Abbr) x2 x3))).(\lambda (_: (pr2 c t x2)).(\lambda (_: ((\forall (b:
-B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x1 x3))))).(let TMP_152 \def
-(Bind Abbr) in (let TMP_153 \def (THead TMP_152 x2 x3) in (let TMP_159 \def
-(\lambda (t1: T).(let TMP_154 \def (Flat Appl) in (let TMP_155 \def (Flat
-Appl) in (let TMP_156 \def (TLRef i) in (let TMP_157 \def (THeads TMP_155 t0
-TMP_156) in (let TMP_158 \def (THead TMP_154 t TMP_157) in (eq T TMP_158
-t1))))))) in (let TMP_167 \def (\lambda (t1: TList).((nf2 c (THeads (Flat
-Appl) t1 (TLRef i))) \to ((eq T (THeads (Flat Appl) t1 (TLRef i)) (THead
-(Bind Abst) x0 x1)) \to (let TMP_160 \def (Flat Appl) in (let TMP_161 \def
-(Flat Appl) in (let TMP_162 \def (TLRef i) in (let TMP_163 \def (THeads
-TMP_161 t1 TMP_162) in (let TMP_164 \def (THead TMP_160 t TMP_163) in (let
-TMP_165 \def (Bind Abbr) in (let TMP_166 \def (THead TMP_165 x2 x3) in (eq T
-TMP_164 TMP_166))))))))))) in (let TMP_180 \def (\lambda (_: (nf2 c (THeads
-(Flat Appl) TNil (TLRef i)))).(\lambda (H13: (eq T (THeads (Flat Appl) TNil
-(TLRef i)) (THead (Bind Abst) x0 x1))).(let TMP_168 \def (TLRef i) in (let
-TMP_169 \def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
-(TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) in (let
-TMP_170 \def (Bind Abst) in (let TMP_171 \def (THead TMP_170 x0 x1) in (let
-H14 \def (eq_ind T TMP_168 TMP_169 I TMP_171 H13) in (let TMP_172 \def (Flat
-Appl) in (let TMP_173 \def (Flat Appl) in (let TMP_174 \def (TLRef i) in (let
-TMP_175 \def (THeads TMP_173 TNil TMP_174) in (let TMP_176 \def (THead
-TMP_172 t TMP_175) in (let TMP_177 \def (Bind Abbr) in (let TMP_178 \def
-(THead TMP_177 x2 x3) in (let TMP_179 \def (eq T TMP_176 TMP_178) in
-(False_ind TMP_179 H14)))))))))))))))) in (let TMP_198 \def (\lambda (t1:
-T).(\lambda (t3: TList).(\lambda (_: (((nf2 c (THeads (Flat Appl) t3 (TLRef
-i))) \to ((eq T (THeads (Flat Appl) t3 (TLRef i)) (THead (Bind Abst) x0 x1))
-\to (eq T (THead (Flat Appl) t (THeads (Flat Appl) t3 (TLRef i))) (THead
-(Bind Abbr) x2 x3)))))).(\lambda (_: (nf2 c (THeads (Flat Appl) (TCons t1 t3)
-(TLRef i)))).(\lambda (H13: (eq T (THeads (Flat Appl) (TCons t1 t3) (TLRef
-i)) (THead (Bind Abst) x0 x1))).(let TMP_181 \def (Flat Appl) in (let TMP_182
-\def (Flat Appl) in (let TMP_183 \def (TLRef i) in (let TMP_184 \def (THeads
-TMP_182 t3 TMP_183) in (let TMP_185 \def (THead TMP_181 t1 TMP_184) in (let
-TMP_186 \def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
-(TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind
-_) \Rightarrow False | (Flat _) \Rightarrow True])])) in (let TMP_187 \def
-(Bind Abst) in (let TMP_188 \def (THead TMP_187 x0 x1) in (let H14 \def
-(eq_ind T TMP_185 TMP_186 I TMP_188 H13) in (let TMP_189 \def (Flat Appl) in
-(let TMP_190 \def (Flat Appl) in (let TMP_191 \def (TCons t1 t3) in (let
-TMP_192 \def (TLRef i) in (let TMP_193 \def (THeads TMP_190 TMP_191 TMP_192)
-in (let TMP_194 \def (THead TMP_189 t TMP_193) in (let TMP_195 \def (Bind
-Abbr) in (let TMP_196 \def (THead TMP_195 x2 x3) in (let TMP_197 \def (eq T
-TMP_194 TMP_196) in (False_ind TMP_197 H14)))))))))))))))))))))))) in (let
-TMP_199 \def (TList_ind TMP_167 TMP_180 TMP_198 t0 H_y H8) in (eq_ind_r T
-TMP_153 TMP_159 TMP_199 t2 H9)))))))))))))))) in (ex4_4_ind T T T T TMP_138
-TMP_141 TMP_142 TMP_145 TMP_151 TMP_200 H7))))))))))))) in (let TMP_293 \def
-(\lambda (H7: (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
+(vs: TList).(TList_ind (\lambda (t: TList).((nfs2 c t) \to (nf2 c (THeads
+(Flat Appl) t (TLRef i))))) (\lambda (_: True).H) (\lambda (t: T).(\lambda
+(t0: TList).(\lambda (H0: (((nfs2 c t0) \to (nf2 c (THeads (Flat Appl) t0
+(TLRef i)))))).(\lambda (H1: (land (nf2 c t) (nfs2 c t0))).(let H2 \def H1 in
+(land_ind (nf2 c t) (nfs2 c t0) (nf2 c (THead (Flat Appl) t (THeads (Flat
+Appl) t0 (TLRef i)))) (\lambda (H3: (nf2 c t)).(\lambda (H4: (nfs2 c
+t0)).(let H_y \def (H0 H4) in (\lambda (t2: T).(\lambda (H5: (pr2 c (THead
+(Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2)).(let H6 \def
+(pr2_gen_appl c t (THeads (Flat Appl) t0 (TLRef i)) t2 H5) in (or3_ind (ex3_2
+T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
+(\lambda (u2: T).(\lambda (_: T).(pr2 c t u2))) (\lambda (_: T).(\lambda (t3:
+T).(pr2 c (THeads (Flat Appl) t0 (TLRef i)) t3)))) (ex4_4 T T T T (\lambda
+(y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THeads (Flat
+Appl) t0 (TLRef i)) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda
+(_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2
+t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
+T).(pr2 c t u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
+(t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1
+t3)))))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
(\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
(_: T).(\lambda (_: T).(eq T (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind
u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2))))))) (\lambda (b:
B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda
-(y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))).(let TMP_203 \def (\lambda
-(b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
-T).(\lambda (_: T).(let TMP_202 \def (eq B b Abst) in (not TMP_202)))))))) in
-(let TMP_209 \def (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda
-(_: T).(\lambda (_: T).(\lambda (_: T).(let TMP_204 \def (Flat Appl) in (let
-TMP_205 \def (TLRef i) in (let TMP_206 \def (THeads TMP_204 t0 TMP_205) in
-(let TMP_207 \def (Bind b) in (let TMP_208 \def (THead TMP_207 y1 z1) in (eq
-T TMP_206 TMP_208)))))))))))) in (let TMP_216 \def (\lambda (b: B).(\lambda
-(_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2:
-T).(let TMP_210 \def (Bind b) in (let TMP_211 \def (Flat Appl) in (let
-TMP_212 \def (S O) in (let TMP_213 \def (lift TMP_212 O u2) in (let TMP_214
-\def (THead TMP_211 TMP_213 z2) in (let TMP_215 \def (THead TMP_210 y2
-TMP_214) in (eq T t2 TMP_215))))))))))))) in (let TMP_217 \def (\lambda (_:
-B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
-(_: T).(pr2 c t u2))))))) in (let TMP_218 \def (\lambda (_: B).(\lambda (y1:
+(y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))) (eq T (THead (Flat Appl) t
+(THeads (Flat Appl) t0 (TLRef i))) t2) (\lambda (H7: (ex3_2 T T (\lambda (u2:
+T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
+T).(\lambda (_: T).(pr2 c t u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c
+(THeads (Flat Appl) t0 (TLRef i)) t3))))).(ex3_2_ind T T (\lambda (u2:
+T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
+T).(\lambda (_: T).(pr2 c t u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c
+(THeads (Flat Appl) t0 (TLRef i)) t3))) (eq T (THead (Flat Appl) t (THeads
+(Flat Appl) t0 (TLRef i))) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda
+(H8: (eq T t2 (THead (Flat Appl) x0 x1))).(\lambda (H9: (pr2 c t
+x0)).(\lambda (H10: (pr2 c (THeads (Flat Appl) t0 (TLRef i)) x1)).(eq_ind_r T
+(THead (Flat Appl) x0 x1) (\lambda (t1: T).(eq T (THead (Flat Appl) t (THeads
+(Flat Appl) t0 (TLRef i))) t1)) (let H11 \def (eq_ind_r T x1 (\lambda (t1:
+T).(pr2 c (THeads (Flat Appl) t0 (TLRef i)) t1)) H10 (THeads (Flat Appl) t0
+(TLRef i)) (H_y x1 H10)) in (eq_ind T (THeads (Flat Appl) t0 (TLRef i))
+(\lambda (t1: T).(eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef
+i))) (THead (Flat Appl) x0 t1))) (let H12 \def (eq_ind_r T x0 (\lambda (t1:
+T).(pr2 c t t1)) H9 t (H3 x0 H9)) in (eq_ind T t (\lambda (t1: T).(eq T
+(THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) (THead (Flat Appl) t1
+(THeads (Flat Appl) t0 (TLRef i))))) (refl_equal T (THead (Flat Appl) t
+(THeads (Flat Appl) t0 (TLRef i)))) x0 (H3 x0 H9))) x1 (H_y x1 H10))) t2
+H8)))))) H7)) (\lambda (H7: (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1:
+T).(\lambda (_: T).(\lambda (_: T).(eq T (THeads (Flat Appl) t0 (TLRef i))
+(THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
+T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t u2))))) (\lambda
+(_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b:
+B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t3))))))))).(ex4_4_ind T T T
+T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
+(THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
+T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
+Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
+(_: T).(pr2 c t u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
+z1 t3))))))) (eq T (THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i)))
+t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3:
+T).(\lambda (H8: (eq T (THeads (Flat Appl) t0 (TLRef i)) (THead (Bind Abst)
+x0 x1))).(\lambda (H9: (eq T t2 (THead (Bind Abbr) x2 x3))).(\lambda (_: (pr2
+c t x2)).(\lambda (_: ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b)
+u) x1 x3))))).(eq_ind_r T (THead (Bind Abbr) x2 x3) (\lambda (t1: T).(eq T
+(THead (Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t1)) (TList_ind
+(\lambda (t1: TList).((nf2 c (THeads (Flat Appl) t1 (TLRef i))) \to ((eq T
+(THeads (Flat Appl) t1 (TLRef i)) (THead (Bind Abst) x0 x1)) \to (eq T (THead
+(Flat Appl) t (THeads (Flat Appl) t1 (TLRef i))) (THead (Bind Abbr) x2
+x3))))) (\lambda (_: (nf2 c (THeads (Flat Appl) TNil (TLRef i)))).(\lambda
+(H13: (eq T (THeads (Flat Appl) TNil (TLRef i)) (THead (Bind Abst) x0
+x1))).(let H14 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee with
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _)
+\Rightarrow False])) I (THead (Bind Abst) x0 x1) H13) in (False_ind (eq T
+(THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))) (THead (Bind Abbr)
+x2 x3)) H14)))) (\lambda (t1: T).(\lambda (t3: TList).(\lambda (_: (((nf2 c
+(THeads (Flat Appl) t3 (TLRef i))) \to ((eq T (THeads (Flat Appl) t3 (TLRef
+i)) (THead (Bind Abst) x0 x1)) \to (eq T (THead (Flat Appl) t (THeads (Flat
+Appl) t3 (TLRef i))) (THead (Bind Abbr) x2 x3)))))).(\lambda (_: (nf2 c
+(THeads (Flat Appl) (TCons t1 t3) (TLRef i)))).(\lambda (H13: (eq T (THeads
+(Flat Appl) (TCons t1 t3) (TLRef i)) (THead (Bind Abst) x0 x1))).(let H14
+\def (eq_ind T (THead (Flat Appl) t1 (THeads (Flat Appl) t3 (TLRef i)))
+(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
+\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) x0
+x1) H13) in (False_ind (eq T (THead (Flat Appl) t (THeads (Flat Appl) (TCons
+t1 t3) (TLRef i))) (THead (Bind Abbr) x2 x3)) H14))))))) t0 H_y H8) t2
+H9))))))))) H7)) (\lambda (H7: (ex6_6 B T T T T T (\lambda (b: B).(\lambda
+(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not
+(eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (THeads (Flat Appl)
+t0 (TLRef i)) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
+T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
+t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
+(\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
+T).(\lambda (_: T).(pr2 c t u2))))))) (\lambda (_: B).(\lambda (y1:
T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
-y2))))))) in (let TMP_221 \def (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
-T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(let TMP_219 \def (Bind
-b) in (let TMP_220 \def (CHead c TMP_219 y2) in (pr2 TMP_220 z1 z2)))))))))
-in (let TMP_222 \def (Flat Appl) in (let TMP_223 \def (Flat Appl) in (let
-TMP_224 \def (TLRef i) in (let TMP_225 \def (THeads TMP_223 t0 TMP_224) in
-(let TMP_226 \def (THead TMP_222 t TMP_225) in (let TMP_227 \def (eq T
-TMP_226 t2) in (let TMP_292 \def (\lambda (x0: B).(\lambda (x1: T).(\lambda
-(x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: (not
-(eq B x0 Abst))).(\lambda (H9: (eq T (THeads (Flat Appl) t0 (TLRef i)) (THead
-(Bind x0) x1 x2))).(\lambda (H10: (eq T t2 (THead (Bind x0) x5 (THead (Flat
-Appl) (lift (S O) O x4) x3)))).(\lambda (_: (pr2 c t x4)).(\lambda (_: (pr2 c
-x1 x5)).(\lambda (_: (pr2 (CHead c (Bind x0) x5) x2 x3)).(let TMP_228 \def
-(Bind x0) in (let TMP_229 \def (Flat Appl) in (let TMP_230 \def (S O) in (let
-TMP_231 \def (lift TMP_230 O x4) in (let TMP_232 \def (THead TMP_229 TMP_231
-x3) in (let TMP_233 \def (THead TMP_228 x5 TMP_232) in (let TMP_239 \def
-(\lambda (t1: T).(let TMP_234 \def (Flat Appl) in (let TMP_235 \def (Flat
-Appl) in (let TMP_236 \def (TLRef i) in (let TMP_237 \def (THeads TMP_235 t0
-TMP_236) in (let TMP_238 \def (THead TMP_234 t TMP_237) in (eq T TMP_238
-t1))))))) in (let TMP_251 \def (\lambda (t1: TList).((nf2 c (THeads (Flat
-Appl) t1 (TLRef i))) \to ((eq T (THeads (Flat Appl) t1 (TLRef i)) (THead
-(Bind x0) x1 x2)) \to (let TMP_240 \def (Flat Appl) in (let TMP_241 \def
-(Flat Appl) in (let TMP_242 \def (TLRef i) in (let TMP_243 \def (THeads
-TMP_241 t1 TMP_242) in (let TMP_244 \def (THead TMP_240 t TMP_243) in (let
-TMP_245 \def (Bind x0) in (let TMP_246 \def (Flat Appl) in (let TMP_247 \def
-(S O) in (let TMP_248 \def (lift TMP_247 O x4) in (let TMP_249 \def (THead
-TMP_246 TMP_248 x3) in (let TMP_250 \def (THead TMP_245 x5 TMP_249) in (eq T
-TMP_244 TMP_250))))))))))))))) in (let TMP_268 \def (\lambda (_: (nf2 c
-(THeads (Flat Appl) TNil (TLRef i)))).(\lambda (H15: (eq T (THeads (Flat
-Appl) TNil (TLRef i)) (THead (Bind x0) x1 x2))).(let TMP_252 \def (TLRef i)
-in (let TMP_253 \def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow
-False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) in
-(let TMP_254 \def (Bind x0) in (let TMP_255 \def (THead TMP_254 x1 x2) in
-(let H16 \def (eq_ind T TMP_252 TMP_253 I TMP_255 H15) in (let TMP_256 \def
-(Flat Appl) in (let TMP_257 \def (Flat Appl) in (let TMP_258 \def (TLRef i)
-in (let TMP_259 \def (THeads TMP_257 TNil TMP_258) in (let TMP_260 \def
-(THead TMP_256 t TMP_259) in (let TMP_261 \def (Bind x0) in (let TMP_262 \def
-(Flat Appl) in (let TMP_263 \def (S O) in (let TMP_264 \def (lift TMP_263 O
-x4) in (let TMP_265 \def (THead TMP_262 TMP_264 x3) in (let TMP_266 \def
-(THead TMP_261 x5 TMP_265) in (let TMP_267 \def (eq T TMP_260 TMP_266) in
-(False_ind TMP_267 H16)))))))))))))))))))) in (let TMP_290 \def (\lambda (t1:
-T).(\lambda (t3: TList).(\lambda (_: (((nf2 c (THeads (Flat Appl) t3 (TLRef
-i))) \to ((eq T (THeads (Flat Appl) t3 (TLRef i)) (THead (Bind x0) x1 x2))
-\to (eq T (THead (Flat Appl) t (THeads (Flat Appl) t3 (TLRef i))) (THead
-(Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))))))).(\lambda (_: (nf2
-c (THeads (Flat Appl) (TCons t1 t3) (TLRef i)))).(\lambda (H15: (eq T (THeads
-(Flat Appl) (TCons t1 t3) (TLRef i)) (THead (Bind x0) x1 x2))).(let TMP_269
-\def (Flat Appl) in (let TMP_270 \def (Flat Appl) in (let TMP_271 \def (TLRef
-i) in (let TMP_272 \def (THeads TMP_270 t3 TMP_271) in (let TMP_273 \def
-(THead TMP_269 t1 TMP_272) in (let TMP_274 \def (\lambda (ee: T).(match ee
-with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _
-_) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _)
-\Rightarrow True])])) in (let TMP_275 \def (Bind x0) in (let TMP_276 \def
-(THead TMP_275 x1 x2) in (let H16 \def (eq_ind T TMP_273 TMP_274 I TMP_276
-H15) in (let TMP_277 \def (Flat Appl) in (let TMP_278 \def (Flat Appl) in
-(let TMP_279 \def (TCons t1 t3) in (let TMP_280 \def (TLRef i) in (let
-TMP_281 \def (THeads TMP_278 TMP_279 TMP_280) in (let TMP_282 \def (THead
-TMP_277 t TMP_281) in (let TMP_283 \def (Bind x0) in (let TMP_284 \def (Flat
-Appl) in (let TMP_285 \def (S O) in (let TMP_286 \def (lift TMP_285 O x4) in
-(let TMP_287 \def (THead TMP_284 TMP_286 x3) in (let TMP_288 \def (THead
-TMP_283 x5 TMP_287) in (let TMP_289 \def (eq T TMP_282 TMP_288) in (False_ind
-TMP_289 H16)))))))))))))))))))))))))))) in (let TMP_291 \def (TList_ind
-TMP_251 TMP_268 TMP_290 t0 H_y H9) in (eq_ind_r T TMP_233 TMP_239 TMP_291 t2
-H10)))))))))))))))))))))))) in (ex6_6_ind B T T T T T TMP_203 TMP_209 TMP_216
-TMP_217 TMP_218 TMP_221 TMP_227 TMP_292 H7))))))))))))))) in (or3_ind TMP_25
-TMP_39 TMP_60 TMP_66 TMP_132 TMP_201 TMP_293
-H6))))))))))))))))))))))))))))))))))) in (land_ind TMP_6 TMP_7 TMP_13 TMP_294
-H2))))))))))))))) in (TList_ind TMP_4 TMP_5 TMP_295 vs))))))).
+y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
+T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1
+z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda
+(_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b
+Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
+T).(\lambda (_: T).(\lambda (_: T).(eq T (THeads (Flat Appl) t0 (TLRef i))
+(THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
+T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
+b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
+B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
+(_: T).(pr2 c t u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
+T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
+(\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
+(_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))) (eq T (THead
+(Flat Appl) t (THeads (Flat Appl) t0 (TLRef i))) t2) (\lambda (x0:
+B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4:
+T).(\lambda (x5: T).(\lambda (_: (not (eq B x0 Abst))).(\lambda (H9: (eq T
+(THeads (Flat Appl) t0 (TLRef i)) (THead (Bind x0) x1 x2))).(\lambda (H10:
+(eq T t2 (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4)
+x3)))).(\lambda (_: (pr2 c t x4)).(\lambda (_: (pr2 c x1 x5)).(\lambda (_:
+(pr2 (CHead c (Bind x0) x5) x2 x3)).(eq_ind_r T (THead (Bind x0) x5 (THead
+(Flat Appl) (lift (S O) O x4) x3)) (\lambda (t1: T).(eq T (THead (Flat Appl)
+t (THeads (Flat Appl) t0 (TLRef i))) t1)) (TList_ind (\lambda (t1:
+TList).((nf2 c (THeads (Flat Appl) t1 (TLRef i))) \to ((eq T (THeads (Flat
+Appl) t1 (TLRef i)) (THead (Bind x0) x1 x2)) \to (eq T (THead (Flat Appl) t
+(THeads (Flat Appl) t1 (TLRef i))) (THead (Bind x0) x5 (THead (Flat Appl)
+(lift (S O) O x4) x3)))))) (\lambda (_: (nf2 c (THeads (Flat Appl) TNil
+(TLRef i)))).(\lambda (H15: (eq T (THeads (Flat Appl) TNil (TLRef i)) (THead
+(Bind x0) x1 x2))).(let H16 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match
+ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _
+_ _) \Rightarrow False])) I (THead (Bind x0) x1 x2) H15) in (False_ind (eq T
+(THead (Flat Appl) t (THeads (Flat Appl) TNil (TLRef i))) (THead (Bind x0) x5
+(THead (Flat Appl) (lift (S O) O x4) x3))) H16)))) (\lambda (t1: T).(\lambda
+(t3: TList).(\lambda (_: (((nf2 c (THeads (Flat Appl) t3 (TLRef i))) \to ((eq
+T (THeads (Flat Appl) t3 (TLRef i)) (THead (Bind x0) x1 x2)) \to (eq T (THead
+(Flat Appl) t (THeads (Flat Appl) t3 (TLRef i))) (THead (Bind x0) x5 (THead
+(Flat Appl) (lift (S O) O x4) x3))))))).(\lambda (_: (nf2 c (THeads (Flat
+Appl) (TCons t1 t3) (TLRef i)))).(\lambda (H15: (eq T (THeads (Flat Appl)
+(TCons t1 t3) (TLRef i)) (THead (Bind x0) x1 x2))).(let H16 \def (eq_ind T
+(THead (Flat Appl) t1 (THeads (Flat Appl) t3 (TLRef i))) (\lambda (ee:
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
+| (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat
+_) \Rightarrow True])])) I (THead (Bind x0) x1 x2) H15) in (False_ind (eq T
+(THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t3) (TLRef i))) (THead
+(Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))) H16))))))) t0 H_y H9)
+t2 H10))))))))))))) H7)) H6))))))) H2)))))) vs)))).
theorem nf2_appl_lref:
\forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (i: nat).((nf2 c
(TLRef i)) \to (nf2 c (THead (Flat Appl) u (TLRef i)))))))
\def
\lambda (c: C).(\lambda (u: T).(\lambda (H: (nf2 c u)).(\lambda (i:
-nat).(\lambda (H0: (nf2 c (TLRef i))).(let TMP_1 \def (TCons u TNil) in (let
-H_y \def (nf2_appls_lref c i H0 TMP_1) in (let TMP_2 \def (nf2 c u) in (let
-TMP_3 \def (conj TMP_2 True H I) in (H_y TMP_3))))))))).
+nat).(\lambda (H0: (nf2 c (TLRef i))).(let H_y \def (nf2_appls_lref c i H0
+(TCons u TNil)) in (H_y (conj (nf2 c u) True H I))))))).
-theorem nf2_lref_abst:
+lemma nf2_lref_abst:
\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (i: nat).((getl i c
(CHead e (Bind Abst) u)) \to (nf2 c (TLRef i))))))
\def
\lambda (c: C).(\lambda (e: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
(H: (getl i c (CHead e (Bind Abst) u))).(\lambda (t2: T).(\lambda (H0: (pr2 c
-(TLRef i) t2)).(let H1 \def (pr2_gen_lref c t2 i H0) in (let TMP_1 \def
-(TLRef i) in (let TMP_2 \def (eq T t2 TMP_1) in (let TMP_5 \def (\lambda (d:
-C).(\lambda (u0: T).(let TMP_3 \def (Bind Abbr) in (let TMP_4 \def (CHead d
-TMP_3 u0) in (getl i c TMP_4))))) in (let TMP_8 \def (\lambda (_: C).(\lambda
-(u0: T).(let TMP_6 \def (S i) in (let TMP_7 \def (lift TMP_6 O u0) in (eq T
-t2 TMP_7))))) in (let TMP_9 \def (ex2_2 C T TMP_5 TMP_8) in (let TMP_10 \def
-(TLRef i) in (let TMP_11 \def (eq T TMP_10 t2) in (let TMP_17 \def (\lambda
-(H2: (eq T t2 (TLRef i))).(let TMP_12 \def (TLRef i) in (let TMP_14 \def
-(\lambda (t: T).(let TMP_13 \def (TLRef i) in (eq T TMP_13 t))) in (let
-TMP_15 \def (TLRef i) in (let TMP_16 \def (refl_equal T TMP_15) in (eq_ind_r
-T TMP_12 TMP_14 TMP_16 t2 H2)))))) in (let TMP_56 \def (\lambda (H2: (ex2_2 C
-T (\lambda (d: C).(\lambda (u0: T).(getl i c (CHead d (Bind Abbr) u0))))
-(\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift (S i) O u0)))))).(let TMP_20
-\def (\lambda (d: C).(\lambda (u0: T).(let TMP_18 \def (Bind Abbr) in (let
-TMP_19 \def (CHead d TMP_18 u0) in (getl i c TMP_19))))) in (let TMP_23 \def
-(\lambda (_: C).(\lambda (u0: T).(let TMP_21 \def (S i) in (let TMP_22 \def
-(lift TMP_21 O u0) in (eq T t2 TMP_22))))) in (let TMP_24 \def (TLRef i) in
-(let TMP_25 \def (eq T TMP_24 t2) in (let TMP_55 \def (\lambda (x0:
-C).(\lambda (x1: T).(\lambda (H3: (getl i c (CHead x0 (Bind Abbr)
-x1))).(\lambda (H4: (eq T t2 (lift (S i) O x1))).(let TMP_26 \def (S i) in
-(let TMP_27 \def (lift TMP_26 O x1) in (let TMP_29 \def (\lambda (t: T).(let
-TMP_28 \def (TLRef i) in (eq T TMP_28 t))) in (let TMP_30 \def (Bind Abst) in
-(let TMP_31 \def (CHead e TMP_30 u) in (let TMP_32 \def (\lambda (c0:
-C).(getl i c c0)) in (let TMP_33 \def (Bind Abbr) in (let TMP_34 \def (CHead
-x0 TMP_33 x1) in (let TMP_35 \def (Bind Abst) in (let TMP_36 \def (CHead e
-TMP_35 u) in (let TMP_37 \def (Bind Abbr) in (let TMP_38 \def (CHead x0
-TMP_37 x1) in (let TMP_39 \def (getl_mono c TMP_36 i H TMP_38 H3) in (let H5
-\def (eq_ind C TMP_31 TMP_32 H TMP_34 TMP_39) in (let TMP_40 \def (Bind Abst)
-in (let TMP_41 \def (CHead e TMP_40 u) in (let TMP_42 \def (\lambda (ee:
-C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow
-(match k with [(Bind b) \Rightarrow (match b with [Abbr \Rightarrow False |
-Abst \Rightarrow True | Void \Rightarrow False]) | (Flat _) \Rightarrow
-False])])) in (let TMP_43 \def (Bind Abbr) in (let TMP_44 \def (CHead x0
-TMP_43 x1) in (let TMP_45 \def (Bind Abst) in (let TMP_46 \def (CHead e
-TMP_45 u) in (let TMP_47 \def (Bind Abbr) in (let TMP_48 \def (CHead x0
-TMP_47 x1) in (let TMP_49 \def (getl_mono c TMP_46 i H TMP_48 H3) in (let H6
-\def (eq_ind C TMP_41 TMP_42 I TMP_44 TMP_49) in (let TMP_50 \def (TLRef i)
-in (let TMP_51 \def (S i) in (let TMP_52 \def (lift TMP_51 O x1) in (let
-TMP_53 \def (eq T TMP_50 TMP_52) in (let TMP_54 \def (False_ind TMP_53 H6) in
-(eq_ind_r T TMP_27 TMP_29 TMP_54 t2 H4))))))))))))))))))))))))))))))))))) in
-(ex2_2_ind C T TMP_20 TMP_23 TMP_25 TMP_55 H2))))))) in (or_ind TMP_2 TMP_9
-TMP_11 TMP_17 TMP_56 H1))))))))))))))))).
+(TLRef i) t2)).(let H1 \def (pr2_gen_lref c t2 i H0) in (or_ind (eq T t2
+(TLRef i)) (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c (CHead d
+(Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift (S i) O
+u0))))) (eq T (TLRef i) t2) (\lambda (H2: (eq T t2 (TLRef i))).(eq_ind_r T
+(TLRef i) (\lambda (t: T).(eq T (TLRef i) t)) (refl_equal T (TLRef i)) t2
+H2)) (\lambda (H2: (ex2_2 C T (\lambda (d: C).(\lambda (u0: T).(getl i c
+(CHead d (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift
+(S i) O u0)))))).(ex2_2_ind C T (\lambda (d: C).(\lambda (u0: T).(getl i c
+(CHead d (Bind Abbr) u0)))) (\lambda (_: C).(\lambda (u0: T).(eq T t2 (lift
+(S i) O u0)))) (eq T (TLRef i) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda
+(H3: (getl i c (CHead x0 (Bind Abbr) x1))).(\lambda (H4: (eq T t2 (lift (S i)
+O x1))).(eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(eq T (TLRef i) t))
+(let H5 \def (eq_ind C (CHead e (Bind Abst) u) (\lambda (c0: C).(getl i c
+c0)) H (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead e (Bind Abst) u) i H
+(CHead x0 (Bind Abbr) x1) H3)) in (let H6 \def (eq_ind C (CHead e (Bind Abst)
+u) (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k
+_) \Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr
+\Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat
+_) \Rightarrow False])])) I (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead e
+(Bind Abst) u) i H (CHead x0 (Bind Abbr) x1) H3)) in (False_ind (eq T (TLRef
+i) (lift (S i) O x1)) H6))) t2 H4))))) H2)) H1)))))))).
-theorem nf2_lift:
+lemma nf2_lift:
\forall (d: C).(\forall (t: T).((nf2 d t) \to (\forall (c: C).(\forall (h:
nat).(\forall (i: nat).((drop h i c d) \to (nf2 c (lift h i t))))))))
\def
\lambda (d: C).(\lambda (t: T).(\lambda (H: ((\forall (t2: T).((pr2 d t t2)
\to (eq T t t2))))).(\lambda (c: C).(\lambda (h: nat).(\lambda (i:
nat).(\lambda (H0: (drop h i c d)).(\lambda (t2: T).(\lambda (H1: (pr2 c
-(lift h i t) t2)).(let H2 \def (pr2_gen_lift c t t2 h i H1 d H0) in (let
-TMP_2 \def (\lambda (t3: T).(let TMP_1 \def (lift h i t3) in (eq T t2
-TMP_1))) in (let TMP_3 \def (\lambda (t3: T).(pr2 d t t3)) in (let TMP_4 \def
-(lift h i t) in (let TMP_5 \def (eq T TMP_4 t2) in (let TMP_16 \def (\lambda
-(x: T).(\lambda (H3: (eq T t2 (lift h i x))).(\lambda (H4: (pr2 d t x)).(let
-TMP_6 \def (lift h i x) in (let TMP_8 \def (\lambda (t0: T).(let TMP_7 \def
-(lift h i t) in (eq T TMP_7 t0))) in (let H_y \def (H x H4) in (let TMP_9
-\def (\lambda (t0: T).(pr2 d t t0)) in (let H5 \def (eq_ind_r T x TMP_9 H4 t
-H_y) in (let TMP_12 \def (\lambda (t0: T).(let TMP_10 \def (lift h i t) in
-(let TMP_11 \def (lift h i t0) in (eq T TMP_10 TMP_11)))) in (let TMP_13 \def
-(lift h i t) in (let TMP_14 \def (refl_equal T TMP_13) in (let TMP_15 \def
-(eq_ind T t TMP_12 TMP_14 x H_y) in (eq_ind_r T TMP_6 TMP_8 TMP_15 t2
-H3))))))))))))) in (ex2_ind T TMP_2 TMP_3 TMP_5 TMP_16 H2))))))))))))))).
+(lift h i t) t2)).(let H2 \def (pr2_gen_lift c t t2 h i H1 d H0) in (ex2_ind
+T (\lambda (t3: T).(eq T t2 (lift h i t3))) (\lambda (t3: T).(pr2 d t t3))
+(eq T (lift h i t) t2) (\lambda (x: T).(\lambda (H3: (eq T t2 (lift h i
+x))).(\lambda (H4: (pr2 d t x)).(eq_ind_r T (lift h i x) (\lambda (t0: T).(eq
+T (lift h i t) t0)) (let H_y \def (H x H4) in (let H5 \def (eq_ind_r T x
+(\lambda (t0: T).(pr2 d t t0)) H4 t H_y) in (eq_ind T t (\lambda (t0: T).(eq
+T (lift h i t) (lift h i t0))) (refl_equal T (lift h i t)) x H_y))) t2 H3))))
+H2)))))))))).
projects / helm.git / blobdiff