- advances in the theory of cofrees

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_leq.ma
index 01bde31ec11a85483440ff7bf90fe8a8bd579d77..bef6eeb7fdc4814dce79689bb57ed14ad24aac2b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_leq.ma
@@ -12,25 +12,25 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/llpx_sn_leq.ma".
+include "basic_2/substitution/llpx_sn_leq.ma".
 include "basic_2/substitution/lleq.ma".
 
 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
 
 (* Properties on equivalence for local environments *************************)
 
-lemma leq_lleq_trans: â\88\80L2,L,T,d. L2 â\8b\95[T, d] L →
-                      â\88\80L1. L1 â\89\83[d, â\88\9e] L2 â\86\92 L1 â\8b\95[T, d] L.
+lemma leq_lleq_trans: â\88\80L2,L,T,d. L2 â\89¡[T, d] L →
+                      â\88\80L1. L1 â\89\83[d, â\88\9e] L2 â\86\92 L1 â\89¡[T, d] L.
 /2 width=3 by leq_llpx_sn_trans/ qed-.
 
-lemma lleq_leq_trans: â\88\80L,L1,T,d. L â\8b\95[T, d] L1 →
-                      â\88\80L2. L1 â\89\83[d, â\88\9e] L2 â\86\92 L â\8b\95[T, d] L2.
+lemma lleq_leq_trans: â\88\80L,L1,T,d. L â\89¡[T, d] L1 →
+                      â\88\80L2. L1 â\89\83[d, â\88\9e] L2 â\86\92 L â\89¡[T, d] L2.
 /2 width=3 by llpx_sn_leq_trans/ qed-.
 
-lemma lleq_leq_repl: â\88\80L1,L2,T,d. L1 â\8b\95[T, d] L2 → ∀K1. K1 ≃[d, ∞] L1 →
-                     â\88\80K2. L2 â\89\83[d, â\88\9e] K2 â\86\92 K1 â\8b\95[T, d] K2.
+lemma lleq_leq_repl: â\88\80L1,L2,T,d. L1 â\89¡[T, d] L2 → ∀K1. K1 ≃[d, ∞] L1 →
+                     â\88\80K2. L2 â\89\83[d, â\88\9e] K2 â\86\92 K1 â\89¡[T, d] K2.
 /2 width=5 by llpx_sn_leq_repl/ qed-.
 
-lemma lleq_bind_repl_SO: â\88\80I1,I2,L1,L2,V1,V2,T. L1.â\93\91{I1}V1 â\8b\95[T, 0] L2.ⓑ{I2}V2 →
-                         â\88\80J1,J2,W1,W2. L1.â\93\91{J1}W1 â\8b\95[T, 1] L2.ⓑ{J2}W2.
+lemma lleq_bind_repl_SO: â\88\80I1,I2,L1,L2,V1,V2,T. L1.â\93\91{I1}V1 â\89¡[T, 0] L2.ⓑ{I2}V2 →
+                         â\88\80J1,J2,W1,W2. L1.â\93\91{J1}W1 â\89¡[T, 1] L2.ⓑ{J2}W2.
 /2 width=5 by llpx_sn_bind_repl_SO/ qed-.