Procedural : tentative update to the new letin cic construction

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / pr2 / clen.ma

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 09a9a3d896de48d497fd6475172998631280336a..ab6e6ef402e4dd497c77cb0388f5611244c4823a 100644 (file)
--- 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