(* This file was automatically generated: do not edit *********************)
+include "LambdaDelta-1/nf2/defs.ma".
-
-include "nf2/defs.ma".
-
-include "pr2/fwd.ma".
+include "LambdaDelta-1/pr2/fwd.ma".
theorem nf2_sort:
\forall (c: C).(\forall (n: nat).(nf2 c (TSort n)))
u x0 t x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 Abst u))) t2
H3)))))) H2)))))))).
+theorem 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).(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
+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 (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 in T
+return (\lambda (_: T).Prop) 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 in T return
+(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
+(_: K).Prop) 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))))))) (\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 in T return (\lambda (_: T).Prop) 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 in T return
+(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow False | (THead k _ _) \Rightarrow (match k in K return (\lambda
+(_: K).Prop) 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: ((\forall (t2: T).((pr2 c u t2)
-\to (eq T u t2))))).(\lambda (i: nat).(\lambda (H0: ((\forall (t2: T).((pr2 c
-(TLRef i) t2) \to (eq T (TLRef i) t2))))).(\lambda (t2: T).(\lambda (H1: (pr2
-c (THead (Flat Appl) u (TLRef i)) t2)).(let H2 \def (pr2_gen_appl c u (TLRef
-i) t2 H1) 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 u u2)))
-(\lambda (_: T).(\lambda (t3: T).(pr2 c (TLRef i) t3)))) (ex4_4 T T T T
-(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
-(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 u
-u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
-T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b) u0) 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 (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 u 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) u (TLRef i)) t2) (\lambda (H3: (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 u u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c
-(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 u u2)))
-(\lambda (_: T).(\lambda (t3: T).(pr2 c (TLRef i) t3))) (eq T (THead (Flat
-Appl) u (TLRef i)) t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H4: (eq T
-t2 (THead (Flat Appl) x0 x1))).(\lambda (H5: (pr2 c u x0)).(\lambda (H6: (pr2
-c (TLRef i) x1)).(eq_ind_r T (THead (Flat Appl) x0 x1) (\lambda (t: T).(eq T
-(THead (Flat Appl) u (TLRef i)) t)) (let H7 \def (eq_ind_r T x1 (\lambda (t:
-T).(pr2 c (TLRef i) t)) H6 (TLRef i) (H0 x1 H6)) in (eq_ind T (TLRef i)
-(\lambda (t: T).(eq T (THead (Flat Appl) u (TLRef i)) (THead (Flat Appl) x0
-t))) (let H8 \def (eq_ind_r T x0 (\lambda (t: T).(pr2 c u t)) H5 u (H x0 H5))
-in (eq_ind T u (\lambda (t: T).(eq T (THead (Flat Appl) u (TLRef i)) (THead
-(Flat Appl) t (TLRef i)))) (refl_equal T (THead (Flat Appl) u (TLRef i))) x0
-(H x0 H5))) x1 (H0 x1 H6))) t2 H4)))))) H3)) (\lambda (H3: (ex4_4 T T T T
-(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
-(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 u
-u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
-T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b) u0) z1
-t3))))))))).(ex4_4_ind T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
-T).(\lambda (_: T).(eq T (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 u u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda
-(_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind
-b) u0) z1 t3))))))) (eq T (THead (Flat Appl) u (TLRef i)) t2) (\lambda (x0:
-T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (H4: (eq T
-(TLRef i) (THead (Bind Abst) x0 x1))).(\lambda (H5: (eq T t2 (THead (Bind
-Abbr) x2 x3))).(\lambda (_: (pr2 c u x2)).(\lambda (_: ((\forall (b:
-B).(\forall (u0: T).(pr2 (CHead c (Bind b) u0) x1 x3))))).(eq_ind_r T (THead
-(Bind Abbr) x2 x3) (\lambda (t: T).(eq T (THead (Flat Appl) u (TLRef i)) t))
-(let H8 \def (eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return
-(\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
-\Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Bind Abst) x0
-x1) H4) in (False_ind (eq T (THead (Flat Appl) u (TLRef i)) (THead (Bind
-Abbr) x2 x3)) H8)) t2 H5))))))))) H3)) (\lambda (H3: (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
-(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 u 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))))))))).(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 (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 u 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) u (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 (H5: (eq
-T (TLRef i) (THead (Bind x0) x1 x2))).(\lambda (H6: (eq T t2 (THead (Bind x0)
-x5 (THead (Flat Appl) (lift (S O) O x4) x3)))).(\lambda (_: (pr2 c u
-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 (t: T).(eq T (THead (Flat Appl) u (TLRef i)) t)) (let H10 \def
-(eq_ind T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_:
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
-(THead _ _ _) \Rightarrow False])) I (THead (Bind x0) x1 x2) H5) in
-(False_ind (eq T (THead (Flat Appl) u (TLRef i)) (THead (Bind x0) x5 (THead
-(Flat Appl) (lift (S O) O x4) x3))) H10)) t2 H6))))))))))))) H3)) H2)))))))).
+ \lambda (c: C).(\lambda (u: T).(\lambda (H: (nf2 c u)).(\lambda (i:
+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:
\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (i: nat).((getl i c