(TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 (CHead c0 (Bind
Abst) u) ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 (CHead c0 (Bind
Abst) u) (TLRef i))))))))).(\lambda (H4: (nf2 c0 (THead (Bind Abst) u
-t0))).(let H5 \def (nf2_gen_abst c0 u t0 H4) in (and_ind (nf2 c0 u) (nf2
+t0))).(let H5 \def (nf2_gen_abst c0 u t0 H4) in (land_ind (nf2 c0 u) (nf2
(CHead c0 (Bind Abst) u) t0) (or3 (ex3_2 T T (\lambda (w: T).(\lambda (u0:
T).(eq T (THead (Bind Abst) u t0) (THead (Bind Abst) w u0)))) (\lambda (w:
T).(\lambda (_: T).(nf2 c0 w))) (\lambda (w: T).(\lambda (u0: T).(nf2 (CHead
t0 (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef
i))))))))).(\lambda (H4: (nf2 c0 (THead (Flat Appl) u t0))).(let H5 \def
-(nf2_gen_flat Appl c0 u t0 H4) in (and_ind (nf2 c0 u) (nf2 c0 t0) (or3 (ex3_2
-T T (\lambda (w: T).(\lambda (u0: T).(eq T (THead (Flat Appl) u t0) (THead
-(Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w))) (\lambda
-(w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst) w) u0)))) (ex nat (\lambda
-(n: nat).(eq T (THead (Flat Appl) u t0) (TSort n)))) (ex3_2 TList nat
-(\lambda (ws: TList).(\lambda (i: nat).(eq T (THead (Flat Appl) u t0) (THeads
-(Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0
-ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef i)))))) (\lambda
-(H6: (nf2 c0 u)).(\lambda (H7: (nf2 c0 t0)).(let H_x \def (H3 H7) in (let H8
-\def H_x in (or3_ind (ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T t0
+(nf2_gen_flat Appl c0 u t0 H4) in (land_ind (nf2 c0 u) (nf2 c0 t0) (or3
+(ex3_2 T T (\lambda (w: T).(\lambda (u0: T).(eq T (THead (Flat Appl) u t0)
(THead (Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w)))
(\lambda (w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst) w) u0)))) (ex nat
-(\lambda (n: nat).(eq T t0 (TSort n)))) (ex3_2 TList nat (\lambda (ws:
-TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws (TLRef i)))))
-(\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_:
+(\lambda (n: nat).(eq T (THead (Flat Appl) u t0) (TSort n)))) (ex3_2 TList
+nat (\lambda (ws: TList).(\lambda (i: nat).(eq T (THead (Flat Appl) u t0)
+(THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
+nat).(nfs2 c0 ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c0 (TLRef
+i)))))) (\lambda (H6: (nf2 c0 u)).(\lambda (H7: (nf2 c0 t0)).(let H_x \def
+(H3 H7) in (let H8 \def H_x in (or3_ind (ex3_2 T T (\lambda (w: T).(\lambda
+(u0: T).(eq T t0 (THead (Bind Abst) w u0)))) (\lambda (w: T).(\lambda (_:
+T).(nf2 c0 w))) (\lambda (w: T).(\lambda (u0: T).(nf2 (CHead c0 (Bind Abst)
+w) u0)))) (ex nat (\lambda (n: nat).(eq T t0 (TSort n)))) (ex3_2 TList nat
+(\lambda (ws: TList).(\lambda (i: nat).(eq T t0 (THeads (Flat Appl) ws (TLRef
+i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c0 ws))) (\lambda (_:
TList).(\lambda (i: nat).(nf2 c0 (TLRef i))))) (or3 (ex3_2 T T (\lambda (w:
T).(\lambda (u0: T).(eq T (THead (Flat Appl) u t0) (THead (Bind Abst) w
u0)))) (\lambda (w: T).(\lambda (_: T).(nf2 c0 w))) (\lambda (w: T).(\lambda