X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fspare.ma;h=040ab8d46cdc5b215a5359641c59df5026b852e5;hb=f5dfc6c24a393a4717a7b40689df768d271d9ac0;hp=463e2d7a397c3b4173577096a0ea3c555c03ac73;hpb=863c1f7bb313c3d9dff08d60c8c7ef7c511263c4;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma
index 463e2d7a3..040ab8d46 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma
@@ -71,14 +71,14 @@ theorem nfs2_tapp:
 \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))).
@@ -404,7 +404,7 @@ u1))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H4: (pc3 c (THead (Flat
 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) 
@@ -435,9 +435,9 @@ H1) in (let H2 \def H_x in (ex_ind T (\lambda (u0: T).(eq T (TLRef j) (lift
 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))))))))).