X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Flleq_leq.ma;h=e23a1521f606b43a1c4ac9b44a3c478aa1f3355f;hb=52e675f555f559c047d5449db7fc89a51b977d35;hp=ea04da02c9b34ff41511393a64fbc5eb2b1f70c1;hpb=75fac6d60f67a4dfa38ea6c2cc45a18eda5d8996;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_leq.ma
index ea04da02c..e23a1521f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_leq.ma
@@ -20,15 +20,15 @@ include "basic_2/multiple/lleq.ma".
 (* Properties on equivalence for local environments *************************)
 
 lemma leq_lleq_trans: ∀L2,L,T,d. L2 ≡[T, d] L →
-                      ∀L1. L1 ≃[d, ∞] L2 → L1 ≡[T, d] L.
+                      ∀L1. L1 ⩬[d, ∞] L2 → L1 ≡[T, d] L.
 /2 width=3 by leq_llpx_sn_trans/ qed-.
 
 lemma lleq_leq_trans: ∀L,L1,T,d. L ≡[T, d] L1 →
-                      ∀L2. L1 ≃[d, ∞] L2 → L ≡[T, d] L2.
+                      ∀L2. L1 ⩬[d, ∞] L2 → L ≡[T, d] L2.
 /2 width=3 by llpx_sn_leq_trans/ qed-.
 
-lemma lleq_leq_repl: ∀L1,L2,T,d. L1 ≡[T, d] L2 → ∀K1. K1 ≃[d, ∞] L1 →
-                     ∀K2. L2 ≃[d, ∞] K2 → K1 ≡[T, d] K2.
+lemma lleq_leq_repl: ∀L1,L2,T,d. L1 ≡[T, d] L2 → ∀K1. K1 ⩬[d, ∞] L1 →
+                     ∀K2. L2 ⩬[d, ∞] K2 → K1 ≡[T, d] K2.
 /2 width=5 by llpx_sn_leq_repl/ qed-.
 
 lemma lleq_bind_repl_SO: ∀I1,I2,L1,L2,V1,V2,T. L1.ⓑ{I1}V1 ≡[T, 0] L2.ⓑ{I2}V2 →