X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fpr2%2Fclen.ma;h=ab6e6ef402e4dd497c77cb0388f5611244c4823a;hb=89519c7b52e06304a94019dd528925300380cdc0;hp=09a9a3d896de48d497fd6475172998631280336a;hpb=e92710b1d9774a6491122668c8463b8658114610;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma
index 09a9a3d89..ab6e6ef40 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma
@@ -100,7 +100,7 @@ v i H5) in (let H6 \def H_x in (or_ind (land (eq nat i O) (eq C (CHead d
 (Bind Abbr) u) (CHead c (Bind b) v))) (ex2 nat (\lambda (j: nat).(eq nat i (S 
 j))) (\lambda (j: nat).(getl j c (CHead d (Bind Abbr) u)))) (pr2 c (THead 
 (Bind b) v t3) (THead (Bind b) v t)) (\lambda (H7: (land (eq nat i O) (eq C 
-(CHead d (Bind Abbr) u) (CHead c (Bind b) v)))).(and_ind (eq nat i O) (eq C 
+(CHead d (Bind Abbr) u) (CHead c (Bind b) v)))).(land_ind (eq nat i O) (eq C 
 (CHead d (Bind Abbr) u) (CHead c (Bind b) v)) (pr2 c (THead (Bind b) v t3) 
 (THead (Bind b) v t)) (\lambda (H8: (eq nat i O)).(\lambda (H9: (eq C (CHead 
 d (Bind Abbr) u) (CHead c (Bind b) v))).(let H10 \def (f_equal C C (\lambda