fixed some regressions

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / ex1 / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma
index 65636c34fd50c7401b774be0f5871cbeebd5dede..9c94c211177c8bcaec4d6b157ba8e6b1f3d24801 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma
@@ -460,7 +460,7 @@ x10 t x12)) H33 (TSort O) H35) in (let H38 \def (eq_ind T x11 (\lambda (t:
 T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
 (lift (S O) O t) x4)) H31 (TSort O) H35) in (let H39 \def (eq_ind C x10 
 (\lambda (c: C).(ty3 g c (TSort O) x12)) H37 (CHead (CSort O) (Bind Abst) 
 T).(pc3 (CHead (CHead (CSort O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) 
 (lift (S O) O t) x4)) H31 (TSort O) H35) in (let H39 \def (eq_ind C x10 
 (\lambda (c: C).(ty3 g c (TSort O) x12)) H37 (CHead (CSort O) (Bind Abst) 

-(TSort O)) H36) in (and_ind (pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) 
+(TSort O)) H36) in (land_ind (pc3 (CHead (CHead (CHead (CSort O) (Bind Abst) 

 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) 
 x0) (\forall (b: B).(\forall (u0: T).(pc3 (CHead (CHead (CHead (CHead (CSort 
 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind 
 (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (TLRef (S (S O))) 
 x0) (\forall (b: B).(\forall (u0: T).(pc3 (CHead (CHead (CHead (CHead (CSort 
 O) (Bind Abst) (TSort O)) (Bind Abst) (TSort O)) (Bind Abst) (TLRef O)) (Bind