- advances in the theory of cofrees

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
index d8a174b825d23a44f9b642ed2d7ba1689bee29bf..dc138a492c89e1a3c6b4a9efabc3f4ad100a16c0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lazyeq_4.ma".
-include "basic_2/relocation/llpx_sn.ma".
+include "basic_2/substitution/llpx_sn.ma".
 
 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
 
@@ -26,7 +26,7 @@ interpretation
    'LazyEq T d L1 L2 = (lleq d T L1 L2).
 
 definition lleq_transitive: predicate (relation4 bind2 lenv term term) ≝
-           λR. â\88\80I,L2,T1,T2. R I L2 T1 T2 â\86\92 â\88\80L1. L1 â\8b\95[T1, 0] L2 → R I L1 T1 T2.
+           λR. â\88\80I,L2,T1,T2. R I L2 T1 T2 â\86\92 â\88\80L1. L1 â\89¡[T1, 0] L2 → R I L1 T1 T2.
 
 (* Basic inversion lemmas ***************************************************)
 
@@ -37,103 +37,103 @@ lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. (
                 ) → (
                    ∀I,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
                    ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V →
-                   K1 â\8b\95[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2
+                   K1 â\89¡[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2
                 ) → (
                    ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2
                 ) → (
                    ∀L1,L2,d,p. |L1| = |L2| → R d (§p) L1 L2
                 ) → (
                    ∀a,I,L1,L2,V,T,d.
-                   L1 â\8b\95[V, d]L2 â\86\92 L1.â\93\91{I}V â\8b\95[T, ⫯d] L2.ⓑ{I}V →
+                   L1 â\89¡[V, d]L2 â\86\92 L1.â\93\91{I}V â\89¡[T, ⫯d] L2.ⓑ{I}V →
                    R d V L1 L2 → R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R d (ⓑ{a,I}V.T) L1 L2
                 ) → (
                    ∀I,L1,L2,V,T,d.
-                   L1 â\8b\95[V, d]L2 â\86\92 L1 â\8b\95[T, d] L2 →
+                   L1 â\89¡[V, d]L2 â\86\92 L1 â\89¡[T, d] L2 →
                    R d V L1 L2 → R d T L1 L2 → R d (ⓕ{I}V.T) L1 L2
                 ) →
-                â\88\80d,T,L1,L2. L1 â\8b\95[T, d] L2 → R d T L1 L2.
+                â\88\80d,T,L1,L2. L1 â\89¡[T, d] L2 → R d T L1 L2.
 #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #T #L1 #L2 #H elim H -L1 -L2 -T -d /2 width=8 by/
 qed-.
 
-lemma lleq_inv_bind: â\88\80a,I,L1,L2,V,T,d. L1 â\8b\95[ⓑ{a,I}V.T, d] L2 →
-                     L1 â\8b\95[V, d] L2 â\88§ L1.â\93\91{I}V â\8b\95[T, ⫯d] L2.ⓑ{I}V.
+lemma lleq_inv_bind: â\88\80a,I,L1,L2,V,T,d. L1 â\89¡[ⓑ{a,I}V.T, d] L2 →
+                     L1 â\89¡[V, d] L2 â\88§ L1.â\93\91{I}V â\89¡[T, ⫯d] L2.ⓑ{I}V.
 /2 width=2 by llpx_sn_inv_bind/ qed-.
 
-lemma lleq_inv_flat: â\88\80I,L1,L2,V,T,d. L1 â\8b\95[ⓕ{I}V.T, d] L2 →
-                     L1 â\8b\95[V, d] L2 â\88§ L1 â\8b\95[T, d] L2.
+lemma lleq_inv_flat: â\88\80I,L1,L2,V,T,d. L1 â\89¡[ⓕ{I}V.T, d] L2 →
+                     L1 â\89¡[V, d] L2 â\88§ L1 â\89¡[T, d] L2.
 /2 width=2 by llpx_sn_inv_flat/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma lleq_fwd_length: â\88\80L1,L2,T,d. L1 â\8b\95[T, d] L2 → |L1| = |L2|.
+lemma lleq_fwd_length: â\88\80L1,L2,T,d. L1 â\89¡[T, d] L2 → |L1| = |L2|.
 /2 width=4 by llpx_sn_fwd_length/ qed-.
 
-lemma lleq_fwd_lref: â\88\80L1,L2,d,i. L1 â\8b\95[#i, d] L2 →
+lemma lleq_fwd_lref: â\88\80L1,L2,d,i. L1 â\89¡[#i, d] L2 →
                      ∨∨ |L1| ≤ i ∧ |L2| ≤ i
                       | yinj i < d
                       | ∃∃I,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I}V &
                                      ⇩[i] L2 ≡ K2.ⓑ{I}V &
-                                      K1 â\8b\95[V, yinj 0] K2 & d ≤ yinj i.
+                                      K1 â\89¡[V, yinj 0] K2 & d ≤ yinj i.
 #L1 #L2 #d #i #H elim (llpx_sn_fwd_lref … H) /2 width=1/
 * /3 width=7 by or3_intro2, ex4_4_intro/
 qed-.
 
-lemma lleq_fwd_ldrop_sn: â\88\80L1,L2,T,d. L1 â\8b\95[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 →
+lemma lleq_fwd_ldrop_sn: â\88\80L1,L2,T,d. L1 â\89¡[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 →
                          ∃K2. ⇩[i] L2 ≡ K2.
 /2 width=7 by llpx_sn_fwd_ldrop_sn/ qed-.
 
-lemma lleq_fwd_ldrop_dx: â\88\80L1,L2,T,d. L1 â\8b\95[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 →
+lemma lleq_fwd_ldrop_dx: â\88\80L1,L2,T,d. L1 â\89¡[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 →
                          ∃K1. ⇩[i] L1 ≡ K1.
 /2 width=7 by llpx_sn_fwd_ldrop_dx/ qed-.
 
 lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d.
-                        L1 â\8b\95[â\93\91{a,I}V.T, d] L2 â\86\92 L1 â\8b\95[V, d] L2.
+                        L1 â\89¡[â\93\91{a,I}V.T, d] L2 â\86\92 L1 â\89¡[V, d] L2.
 /2 width=4 by llpx_sn_fwd_bind_sn/ qed-.
 
 lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,d.
-                        L1 â\8b\95[â\93\91{a,I}V.T, d] L2 â\86\92 L1.â\93\91{I}V â\8b\95[T, ⫯d] L2.ⓑ{I}V.
+                        L1 â\89¡[â\93\91{a,I}V.T, d] L2 â\86\92 L1.â\93\91{I}V â\89¡[T, ⫯d] L2.ⓑ{I}V.
 /2 width=2 by llpx_sn_fwd_bind_dx/ qed-.
 
 lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,d.
-                        L1 â\8b\95[â\93\95{I}V.T, d] L2 â\86\92 L1 â\8b\95[V, d] L2.
+                        L1 â\89¡[â\93\95{I}V.T, d] L2 â\86\92 L1 â\89¡[V, d] L2.
 /2 width=3 by llpx_sn_fwd_flat_sn/ qed-.
 
 lemma lleq_fwd_flat_dx: ∀I,L1,L2,V,T,d.
-                        L1 â\8b\95[â\93\95{I}V.T, d] L2 â\86\92 L1 â\8b\95[T, d] L2.
+                        L1 â\89¡[â\93\95{I}V.T, d] L2 â\86\92 L1 â\89¡[T, d] L2.
 /2 width=3 by llpx_sn_fwd_flat_dx/ qed-.
 
 (* Basic properties *********************************************************)
 
-lemma lleq_sort: â\88\80L1,L2,d,k. |L1| = |L2| â\86\92 L1 â\8b\95[⋆k, d] L2.
+lemma lleq_sort: â\88\80L1,L2,d,k. |L1| = |L2| â\86\92 L1 â\89¡[⋆k, d] L2.
 /2 width=1 by llpx_sn_sort/ qed.
 
-lemma lleq_skip: â\88\80L1,L2,d,i. yinj i < d â\86\92 |L1| = |L2| â\86\92 L1 â\8b\95[#i, d] L2.
+lemma lleq_skip: â\88\80L1,L2,d,i. yinj i < d â\86\92 |L1| = |L2| â\86\92 L1 â\89¡[#i, d] L2.
 /2 width=1 by llpx_sn_skip/ qed.
 
 lemma lleq_lref: ∀I,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
                  ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V →
-                 K1 â\8b\95[V, 0] K2 â\86\92 L1 â\8b\95[#i, d] L2.
+                 K1 â\89¡[V, 0] K2 â\86\92 L1 â\89¡[#i, d] L2.
 /2 width=9 by llpx_sn_lref/ qed.
 
-lemma lleq_free: â\88\80L1,L2,d,i. |L1| â\89¤ i â\86\92 |L2| â\89¤ i â\86\92 |L1| = |L2| â\86\92 L1 â\8b\95[#i, d] L2.
+lemma lleq_free: â\88\80L1,L2,d,i. |L1| â\89¤ i â\86\92 |L2| â\89¤ i â\86\92 |L1| = |L2| â\86\92 L1 â\89¡[#i, d] L2.
 /2 width=1 by llpx_sn_free/ qed.
 
-lemma lleq_gref: â\88\80L1,L2,d,p. |L1| = |L2| â\86\92 L1 â\8b\95[§p, d] L2.
+lemma lleq_gref: â\88\80L1,L2,d,p. |L1| = |L2| â\86\92 L1 â\89¡[§p, d] L2.
 /2 width=1 by llpx_sn_gref/ qed.
 
 lemma lleq_bind: ∀a,I,L1,L2,V,T,d.
-                 L1 â\8b\95[V, d] L2 â\86\92 L1.â\93\91{I}V â\8b\95[T, ⫯d] L2.ⓑ{I}V →
-                 L1 â\8b\95[ⓑ{a,I}V.T, d] L2.
+                 L1 â\89¡[V, d] L2 â\86\92 L1.â\93\91{I}V â\89¡[T, ⫯d] L2.ⓑ{I}V →
+                 L1 â\89¡[ⓑ{a,I}V.T, d] L2.
 /2 width=1 by llpx_sn_bind/ qed.
 
 lemma lleq_flat: ∀I,L1,L2,V,T,d.
-                 L1 â\8b\95[V, d] L2 â\86\92 L1 â\8b\95[T, d] L2 â\86\92 L1 â\8b\95[ⓕ{I}V.T, d] L2.
+                 L1 â\89¡[V, d] L2 â\86\92 L1 â\89¡[T, d] L2 â\86\92 L1 â\89¡[ⓕ{I}V.T, d] L2.
 /2 width=1 by llpx_sn_flat/ qed.
 
 lemma lleq_refl: ∀d,T. reflexive … (lleq d T).
 /2 width=1 by llpx_sn_refl/ qed.
 
-lemma lleq_Y: â\88\80L1,L2,T. |L1| = |L2| â\86\92 L1 â\8b\95[T, ∞] L2.
+lemma lleq_Y: â\88\80L1,L2,T. |L1| = |L2| â\86\92 L1 â\89¡[T, ∞] L2.
 /2 width=1 by llpx_sn_Y/ qed.
 
 lemma lleq_sym: ∀d,T. symmetric … (lleq d T).
@@ -141,20 +141,20 @@ lemma lleq_sym: ∀d,T. symmetric … (lleq d T).
 /2 width=7 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/
 qed-.
 
-lemma lleq_ge_up: â\88\80L1,L2,U,dt. L1 â\8b\95[U, dt] L2 →
+lemma lleq_ge_up: â\88\80L1,L2,U,dt. L1 â\89¡[U, dt] L2 →
                   ∀T,d,e. ⇧[d, e] T ≡ U →
-                  dt â\89¤ d + e â\86\92 L1 â\8b\95[U, d] L2.
+                  dt â\89¤ d + e â\86\92 L1 â\89¡[U, d] L2.
 /2 width=6 by llpx_sn_ge_up/ qed-.
 
-lemma lleq_ge: â\88\80L1,L2,T,d1. L1 â\8b\95[T, d1] L2 â\86\92 â\88\80d2. d1 â\89¤ d2 â\86\92 L1 â\8b\95[T, d2] L2.
+lemma lleq_ge: â\88\80L1,L2,T,d1. L1 â\89¡[T, d1] L2 â\86\92 â\88\80d2. d1 â\89¤ d2 â\86\92 L1 â\89¡[T, d2] L2.
 /2 width=3 by llpx_sn_ge/ qed-.
 
-lemma lleq_bind_O: â\88\80a,I,L1,L2,V,T. L1 â\8b\95[V, 0] L2 â\86\92 L1.â\93\91{I}V â\8b\95[T, 0] L2.ⓑ{I}V →
-                   L1 â\8b\95[ⓑ{a,I}V.T, 0] L2.
+lemma lleq_bind_O: â\88\80a,I,L1,L2,V,T. L1 â\89¡[V, 0] L2 â\86\92 L1.â\93\91{I}V â\89¡[T, 0] L2.ⓑ{I}V →
+                   L1 â\89¡[ⓑ{a,I}V.T, 0] L2.
 /2 width=1 by llpx_sn_bind_O/ qed-.
 
 (* Advancded properties on lazy pointwise exyensions ************************)
 
 lemma llpx_sn_lrefl: ∀R. (∀I,L. reflexive … (R I L)) →
-                     â\88\80L1,L2,T,d. L1 â\8b\95[T, d] L2 → llpx_sn R d T L1 L2.
+                     â\88\80L1,L2,T,d. L1 â\89¡[T, d] L2 → llpx_sn R d T L1 L2.
 /2 width=3 by llpx_sn_co/ qed-.