X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fmultiple%2Fllpx_sn.ma;h=fa2a4a3e5e17c58aceee17ea4e864a3e4694d0bb;hp=9eb82fa142ca12123eed1a34b02e2ef9f56d4f20;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hpb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/llpx_sn.ma
index 9eb82fa14..fa2a4a3e5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/llpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/llpx_sn.ma
@@ -12,7 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2A/ynat/ynat_plus.ma".
+include "ground_2/xoa/ex_5_5.ma".
+include "ground_2/ynat/ynat_plus.ma".
 include "basic_2A/substitution/drop.ma".
 
 (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
@@ -26,7 +27,7 @@ inductive llpx_sn (R:relation3 lenv term term): relation4 ynat term lenv lenv 
 | llpx_sn_free: ∀L1,L2,l,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → llpx_sn R l (#i) L1 L2
 | llpx_sn_gref: ∀L1,L2,l,p. |L1| = |L2| → llpx_sn R l (§p) L1 L2
 | llpx_sn_bind: ∀a,I,L1,L2,V,T,l.
-                llpx_sn R l V L1 L2 → llpx_sn R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
+                llpx_sn R l V L1 L2 → llpx_sn R (↑l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
                 llpx_sn R l (ⓑ{a,I}V.T) L1 L2
 | llpx_sn_flat: ∀I,L1,L2,V,T,l.
                 llpx_sn R l V L1 L2 → llpx_sn R l T L1 L2 → llpx_sn R l (ⓕ{I}V.T) L1 L2
@@ -36,7 +37,7 @@ inductive llpx_sn (R:relation3 lenv term term): relation4 ynat term lenv lenv 
 
 fact llpx_sn_inv_bind_aux: ∀R,L1,L2,X,l. llpx_sn R l X L1 L2 →
                            ∀a,I,V,T. X = ⓑ{a,I}V.T →
-                           llpx_sn R l V L1 L2 ∧ llpx_sn R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
+                           llpx_sn R l V L1 L2 ∧ llpx_sn R (↑l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
 #R #L1 #L2 #X #l * -L1 -L2 -X -l
 [ #L1 #L2 #l #k #_ #b #J #W #U #H destruct
 | #L1 #L2 #l #i #_ #_ #b #J #W #U #H destruct
@@ -49,7 +50,7 @@ fact llpx_sn_inv_bind_aux: ∀R,L1,L2,X,l. llpx_sn R l X L1 L2 →
 qed-.
 
 lemma llpx_sn_inv_bind: ∀R,a,I,L1,L2,V,T,l. llpx_sn R l (ⓑ{a,I}V.T) L1 L2 →
-                        llpx_sn R l V L1 L2 ∧ llpx_sn R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
+                        llpx_sn R l V L1 L2 ∧ llpx_sn R (↑l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
 /2 width=4 by llpx_sn_inv_bind_aux/ qed-.
 
 fact llpx_sn_inv_flat_aux: ∀R,L1,L2,X,l. llpx_sn R l X L1 L2 →
@@ -126,7 +127,7 @@ lemma llpx_sn_fwd_bind_sn: ∀R,a,I,L1,L2,V,T,l. llpx_sn R l (ⓑ{a,I}V.T) L1 L2
 qed-.
 
 lemma llpx_sn_fwd_bind_dx: ∀R,a,I,L1,L2,V,T,l. llpx_sn R l (ⓑ{a,I}V.T) L1 L2 →
-                           llpx_sn R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
+                           llpx_sn R (↑l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V).
 #R #a #I #L1 #L2 #V #T #l #H elim (llpx_sn_inv_bind … H) -H //
 qed-.