milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / multiple / lleq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lleq.ma
index f8c737dc531b8342da29f3654582de1b6a90a5f7..928058cfb6f1d579a83cec972dd50c1588bfb1f4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lleq.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/xoa/ex_4_4.ma".
 include "basic_2A/notation/relations/lazyeq_4.ma".
 include "basic_2A/multiple/llpx_sn.ma".
 
@@ -44,8 +45,8 @@ lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. (
                    ∀L1,L2,l,p. |L1| = |L2| → R l (§p) L1 L2
                 ) → (
                    ∀a,I,L1,L2,V,T,l.
-                   L1 â\89¡[V, l]L2 â\86\92 L1.â\93\91{I}V â\89¡[T, ⫯l] L2.ⓑ{I}V →
-                   R l V L1 L2 â\86\92 R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R l (ⓑ{a,I}V.T) L1 L2
+                   L1 â\89¡[V, l]L2 â\86\92 L1.â\93\91{I}V â\89¡[T, â\86\91l] L2.ⓑ{I}V →
+                   R l V L1 L2 â\86\92 R (â\86\91l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R l (ⓑ{a,I}V.T) L1 L2
                 ) → (
                    ∀I,L1,L2,V,T,l.
                    L1 ≡[V, l]L2 → L1 ≡[T, l] L2 →
@@ -56,7 +57,7 @@ lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. (
 qed-.
 
 lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,l. L1 ≡[ⓑ{a,I}V.T, l] L2 →
-                     L1 â\89¡[V, l] L2 â\88§ L1.â\93\91{I}V â\89¡[T, ⫯l] L2.ⓑ{I}V.
+                     L1 â\89¡[V, l] L2 â\88§ L1.â\93\91{I}V â\89¡[T, â\86\91l] L2.ⓑ{I}V.
 /2 width=2 by llpx_sn_inv_bind/ qed-.
 
 lemma lleq_inv_flat: ∀I,L1,L2,V,T,l. L1 ≡[ⓕ{I}V.T, l] L2 →
@@ -91,7 +92,7 @@ lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,l.
 /2 width=4 by llpx_sn_fwd_bind_sn/ qed-.
 
 lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,l.
-                        L1 â\89¡[â\93\91{a,I}V.T, l] L2 â\86\92 L1.â\93\91{I}V â\89¡[T, ⫯l] L2.ⓑ{I}V.
+                        L1 â\89¡[â\93\91{a,I}V.T, l] L2 â\86\92 L1.â\93\91{I}V â\89¡[T, â\86\91l] L2.ⓑ{I}V.
 /2 width=2 by llpx_sn_fwd_bind_dx/ qed-.
 
 lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,l.
@@ -122,7 +123,7 @@ lemma lleq_gref: ∀L1,L2,l,p. |L1| = |L2| → L1 ≡[§p, l] L2.
 /2 width=1 by llpx_sn_gref/ qed.
 
 lemma lleq_bind: ∀a,I,L1,L2,V,T,l.
-                 L1 â\89¡[V, l] L2 â\86\92 L1.â\93\91{I}V â\89¡[T, ⫯l] L2.ⓑ{I}V →
+                 L1 â\89¡[V, l] L2 â\86\92 L1.â\93\91{I}V â\89¡[T, â\86\91l] L2.ⓑ{I}V →
                  L1 ≡[ⓑ{a,I}V.T, l] L2.
 /2 width=1 by llpx_sn_bind/ qed.