(* This file was automatically generated: do not edit *********************)
-include "nf2/defs.ma".
+include "LambdaDelta-1/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 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).(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 (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:
\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)))))))
(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
-(and_ind (nf2 c t) (nfs2 c t0) (nf2 c (THead (Flat Appl) t (THeads (Flat
+(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