- ldrop is now drop as in basic_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / multiple / lleq_leq.ma

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 ea04da02c9b34ff41511393a64fbc5eb2b1f70c1..e23a1521f606b43a1c4ac9b44a3c478aa1f3355f 100644 (file)
--- 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 →
-                      â\88\80L1. L1 â\89\83[d, ∞] L2 → L1 ≡[T, d] L.
+                      â\88\80L1. 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 →
-                      â\88\80L2. L1 â\89\83[d, ∞] L2 → L ≡[T, d] L2.
+                      â\88\80L2. L1 ⩬[d, ∞] L2 → L ≡[T, d] L2.
 /2 width=3 by llpx_sn_leq_trans/ qed-.
 
-lemma lleq_leq_repl: â\88\80L1,L2,T,d. L1 â\89¡[T, d] L2 â\86\92 â\88\80K1. K1 â\89\83[d, ∞] L1 →
-                     â\88\80K2. L2 â\89\83[d, ∞] K2 → K1 ≡[T, d] K2.
+lemma lleq_leq_repl: â\88\80L1,L2,T,d. L1 â\89¡[T, d] L2 â\86\92 â\88\80K1. K1 ⩬[d, ∞] L1 →
+                     â\88\80K2. 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 →