X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta%2Fty3%2Fsubst1.ma;h=094ce7ecb3e0c78d315c2c94ee017e11c2b7c9b1;hb=2cd3e5e157c86a07666eb7501b5050cbafdfe6b1;hp=eb09bb82992a00c5f90c44ca5de0848507e105c8;hpb=745585f18b0f5232214e1199ca1d4985f0238836;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/subst1.ma
index eb09bb829..094ce7ecb 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/subst1.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/subst1.ma
@@ -498,7 +498,7 @@ Appl) w v) (lift (S O) d y1)))) (\lambda (_: T).(\lambda (y2: T).(subst1 d u0
 (y1: T).(\lambda (y2: T).(ty3 g a y1 y2)))) (\lambda (x4: T).(\lambda (x5: 
 T).(\lambda (H15: (eq T (lift (S O) d x1) (THead (Bind Abst) x4 
 x5))).(\lambda (H16: (subst1 d u0 u x4)).(\lambda (H17: (subst1 (s (Bind 
-Abst) d) u0 t x5)).(let H18 \def (sym_equal T (lift (S O) d x1) (THead (Bind 
+Abst) d) u0 t x5)).(let H18 \def (sym_eq T (lift (S O) d x1) (THead (Bind 
 Abst) x4 x5) H15) in (ex3_2_ind T T (\lambda (y: T).(\lambda (z: T).(eq T x1 
 (THead (Bind Abst) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T x4 (lift (S 
 O) d y)))) (\lambda (_: T).(\lambda (z: T).(eq T x5 (lift (S O) (S d) z))))