Procedural : tentative update to the new letin cic construction

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / ty3 / nf2.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma
index f76e4928957c5308bd1e97ddaaeaf5f314dfc61b..0c23d2956a4d062ca0ad009b96891303e293ee20 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma
@@ -257,7 +257,7 @@ x3)).(\lambda (H12: (ty3 g (CHead c (Bind Abst) w) u x2)).(ex3_2_ind T T
 (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) w) v)))) (\lambda 
 (x4: T).(\lambda (x5: T).(\lambda (H13: (pc3 c (THead (Bind Abst) x0 x4) 
 (THead (Bind Abst) w u))).(\lambda (_: (ty3 g c x0 x5)).(\lambda (H15: (ty3 g 
-(CHead c (Bind Abst) x0) x1 x4)).(and_ind (pc3 c x0 w) (\forall (b: 
+(CHead c (Bind Abst) x0) x1 x4)).(land_ind (pc3 c x0 w) (\forall (b: 
 B).(\forall (u0: T).(pc3 (CHead c (Bind b) u0) x4 u))) (ex4_2 T T (\lambda 
 (v: T).(\lambda (_: T).(eq T (THead (Bind Abst) x0 x1) (THead (Bind Abst) w 
 v)))) (\lambda (_: T).(\lambda (w0: T).(ty3 g c w w0))) (\lambda (v: