X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfeq.ma;h=f7375afbc829971da4837150469b46705fab7f0d;hb=5c186c72f508da0849058afeecc6877cd9ed6303;hp=f108bc5af9f5bc2fe04fe8bad7c102da228036ff;hpb=75f395f0febd02de8e0f881d918a8812b1425c8d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma
index f108bc5af..f7375afbc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma
@@ -56,11 +56,11 @@ elim (lfxs_inv_zero_pair_dx … H) -H #K1 #X #HK12 #HX #H destruct
 /2 width=3 by ex2_intro/
 qed-.
 
-lemma lfeq_inv_lref_bind_sn: ∀I1,K1,L2,i. K1.ⓘ{I1} ≡[#⫯i] L2 →
+lemma lfeq_inv_lref_bind_sn: ∀I1,K1,L2,i. K1.ⓘ{I1} ≡[#↑i] L2 →
                              ∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ{I2}.
 /2 width=2 by lfxs_inv_lref_bind_sn/ qed-.
 
-lemma lfeq_inv_lref_bind_dx: ∀I2,K2,L1,i. L1 ≡[#⫯i] K2.ⓘ{I2} →
+lemma lfeq_inv_lref_bind_dx: ∀I2,K2,L1,i. L1 ≡[#↑i] K2.ⓘ{I2} →
                              ∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ{I1}.
 /2 width=2 by lfxs_inv_lref_bind_dx/ qed-.