X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fnf2%2Fprops.ma;h=a801ea1bb970a2d86d88788a5a854c575dbed88a;hb=f73bd1c1cdd504c2a991071505b2e4f541791a7f;hp=05f2b77f116ca04df5a4b0771daccf75be442711;hpb=d0982534aee06a30f91a06d2f3e82834b132a3d3;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma
index 05f2b77f1..a801ea1bb 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma
@@ -14,9 +14,9 @@
 
 (* 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)))
@@ -84,6 +84,24 @@ b) u0) t x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T
 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)))))))
@@ -93,7 +111,7 @@ 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