\def
\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 (and_ind (nf2 c t) True (land True
+(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 (and_ind (nf2 c t0) (nfs2 c
+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 (and_ind (nfs2 c t1) (nf2 c t) (land (land (nf2 c t0) (nfs2 c
+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))).
Appl) t (THead (Bind Abst) x0 x1)) u1)).(\lambda (H5: (ty3 g c (THeads (Flat
Appl) t0 (TLRef i)) (THead (Bind Abst) x0 x1))).(\lambda (_: (ty3 g c t
x0)).(\lambda (H7: (nf2 c (THead (Bind Abst) x0 x1))).(let H8 \def
-(nf2_gen_abst c x0 x1 H7) in (and_ind (nf2 c x0) (nf2 (CHead c (Bind Abst)
+(nf2_gen_abst c x0 x1 H7) in (land_ind (nf2 c x0) (nf2 (CHead c (Bind Abst)
x0) x1) (ex2 T (\lambda (u: T).(nf2 c (lift (S i) O u))) (\lambda (u: T).(pc3
c (THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O u))) u1)))
(\lambda (H9: (nf2 c x0)).(\lambda (H10: (nf2 (CHead c (Bind Abst) x0)
i) O x))).(let H_x0 \def (lift_gen_lref x O (S i) j H3) in (let H4 \def H_x0
in (or_ind (land (lt j O) (eq T x (TLRef j))) (land (le (plus O (S i)) j) (eq
T x (TLRef (minus j (S i))))) (lt i j) (\lambda (H5: (land (lt j O) (eq T x
-(TLRef j)))).(and_ind (lt j O) (eq T x (TLRef j)) (lt i j) (\lambda (H6: (lt
+(TLRef j)))).(land_ind (lt j O) (eq T x (TLRef j)) (lt i j) (\lambda (H6: (lt
j O)).(\lambda (_: (eq T x (TLRef j))).(lt_x_O j H6 (lt i j)))) H5)) (\lambda
-(H5: (land (le (plus O (S i)) j) (eq T x (TLRef (minus j (S i)))))).(and_ind
+(H5: (land (le (plus O (S i)) j) (eq T x (TLRef (minus j (S i)))))).(land_ind
(le (plus O (S i)) j) (eq T x (TLRef (minus j (S i)))) (lt i j) (\lambda (H6:
(le (plus O (S i)) j)).(\lambda (_: (eq T x (TLRef (minus j (S i))))).H6))
H5)) H4))))) H2))))))))).