notational change of lift, drop, and gget

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
index 006abfec3a2f2b275b53a37d59bab934780dc22b..c78445befc43a5b6b69b42ab3588821e77f391a3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "ground_2/ynat/ynat_plus.ma".
-include "basic_2/substitution/ldrop.ma".
+include "basic_2/substitution/drop.ma".
 
 (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
 
@@ -21,7 +21,7 @@ inductive llpx_sn (R:relation3 lenv term term): relation4 ynat term lenv lenv 
 | llpx_sn_sort: ∀L1,L2,d,k. |L1| = |L2| → llpx_sn R d (⋆k) L1 L2
 | llpx_sn_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → llpx_sn R d (#i) L1 L2
 | llpx_sn_lref: ∀I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
-                â\87©[i] L1 â\89¡ K1.â\93\91{I}V1 â\86\92 â\87©[i] L2 ≡ K2.ⓑ{I}V2 →
+                â¬\87[i] L1 â\89¡ K1.â\93\91{I}V1 â\86\92 â¬\87[i] L2 ≡ K2.ⓑ{I}V2 →
                 llpx_sn R (yinj 0) V1 K1 K2 → R K1 V1 V2 → llpx_sn R d (#i) L1 L2
 | llpx_sn_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → llpx_sn R d (#i) L1 L2
 | llpx_sn_gref: ∀L1,L2,d,p. |L1| = |L2| → llpx_sn R d (§p) L1 L2
@@ -75,28 +75,28 @@ lemma llpx_sn_inv_flat: ∀R,I,L1,L2,V,T,d. llpx_sn R d (ⓕ{I}V.T) L1 L2 →
 lemma llpx_sn_fwd_length: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → |L1| = |L2|.
 #R #L1 #L2 #T #d #H elim H -L1 -L2 -T -d //
 #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #HLK1 #HLK2 #_ #_ #HK12
-lapply (ldrop_fwd_length … HLK1) -HLK1
-lapply (ldrop_fwd_length … HLK2) -HLK2
+lapply (drop_fwd_length … HLK1) -HLK1
+lapply (drop_fwd_length … HLK2) -HLK2
 normalize //
 qed-.
 
-lemma llpx_sn_fwd_ldrop_sn: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
-                            â\88\80K1,i. â\87©[i] L1 â\89¡ K1 â\86\92 â\88\83K2. â\87©[i] L2 ≡ K2.
+lemma llpx_sn_fwd_drop_sn: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
+                            â\88\80K1,i. â¬\87[i] L1 â\89¡ K1 â\86\92 â\88\83K2. â¬\87[i] L2 ≡ K2.
 #R #L1 #L2 #T #d #H #K1 #i #HLK1 lapply (llpx_sn_fwd_length … H) -H
-#HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/
+#HL12 lapply (drop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by drop_O1_le/
 qed-.
 
-lemma llpx_sn_fwd_ldrop_dx: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
-                            â\88\80K2,i. â\87©[i] L2 â\89¡ K2 â\86\92 â\88\83K1. â\87©[i] L1 ≡ K1.
+lemma llpx_sn_fwd_drop_dx: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 →
+                            â\88\80K2,i. â¬\87[i] L2 â\89¡ K2 â\86\92 â\88\83K1. â¬\87[i] L1 ≡ K1.
 #R #L1 #L2 #T #d #H #K2 #i #HLK2 lapply (llpx_sn_fwd_length … H) -H
-#HL12 lapply (ldrop_fwd_length_le2 … HLK2) -HLK2 /2 width=1 by ldrop_O1_le/
+#HL12 lapply (drop_fwd_length_le2 … HLK2) -HLK2 /2 width=1 by drop_O1_le/
 qed-.
 
 fact llpx_sn_fwd_lref_aux: ∀R,L1,L2,X,d. llpx_sn R d X L1 L2 → ∀i. X = #i →
                            ∨∨ |L1| ≤ i ∧ |L2| ≤ i
                             | yinj i < d
-                            | â\88\83â\88\83I,K1,K2,V1,V2. â\87©[i] L1 ≡ K1.ⓑ{I}V1 &
-                                               â\87©[i] L2 ≡ K2.ⓑ{I}V2 &
+                            | â\88\83â\88\83I,K1,K2,V1,V2. â¬\87[i] L1 ≡ K1.ⓑ{I}V1 &
+                                               â¬\87[i] L2 ≡ K2.ⓑ{I}V2 &
                                                llpx_sn R (yinj 0) V1 K1 K2 &
                                                R K1 V1 V2 & d ≤ yinj i.
 #R #L1 #L2 #X #d * -L1 -L2 -X -d
@@ -114,8 +114,8 @@ qed-.
 lemma llpx_sn_fwd_lref: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 →
                         ∨∨ |L1| ≤ i ∧ |L2| ≤ i
                          | yinj i < d
-                         | â\88\83â\88\83I,K1,K2,V1,V2. â\87©[i] L1 ≡ K1.ⓑ{I}V1 &
-                                            â\87©[i] L2 ≡ K2.ⓑ{I}V2 &
+                         | â\88\83â\88\83I,K1,K2,V1,V2. â¬\87[i] L1 ≡ K1.ⓑ{I}V1 &
+                                            â¬\87[i] L2 ≡ K2.ⓑ{I}V2 &
                                             llpx_sn R (yinj 0) V1 K1 K2 &
                                             R K1 V1 V2 & d ≤ yinj i.
 /2 width=3 by llpx_sn_fwd_lref_aux/ qed-.
@@ -145,14 +145,14 @@ lemma llpx_sn_fwd_pair_sn: ∀R,I,L1,L2,V,T,d. llpx_sn R d (②{I}V.T) L1 L2 →
 #R * /2 width=4 by llpx_sn_fwd_flat_sn, llpx_sn_fwd_bind_sn/
 qed-.
 
-(* Basic_properties *********************************************************)
+(* Basic properties *********************************************************)
 
 lemma llpx_sn_refl: ∀R. (∀L. reflexive … (R L)) → ∀T,L,d. llpx_sn R d T L L.
 #R #HR #T #L @(f2_ind … rfw … L T) -L -T
 #n #IH #L * * /3 width=1 by llpx_sn_sort, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
 #i #Hn elim (lt_or_ge i (|L|)) /2 width=1 by llpx_sn_free/
 #HiL #d elim (ylt_split i d) /2 width=1 by llpx_sn_skip/
-elim (ldrop_O1_lt … HiL) -HiL destruct /4 width=9 by llpx_sn_lref, ldrop_fwd_rfw/
+elim (drop_O1_lt … HiL) -HiL destruct /4 width=9 by llpx_sn_lref, drop_fwd_rfw/
 qed-.
 
 lemma llpx_sn_Y: ∀R,T,L1,L2. |L1| = |L2| → llpx_sn R (∞) T L1 L2.
@@ -163,7 +163,7 @@ lemma llpx_sn_Y: ∀R,T,L1,L2. |L1| = |L2| → llpx_sn R (∞) T L1 L2.
 @IH -IH // normalize /2 width=1 by eq_f2/
 qed-.
 
-lemma llpx_sn_ge_up: â\88\80R,L1,L2,U,dt. llpx_sn R dt U L1 L2 â\86\92 â\88\80T,d,e. â\87§[d, e] T ≡ U →
+lemma llpx_sn_ge_up: â\88\80R,L1,L2,U,dt. llpx_sn R dt U L1 L2 â\86\92 â\88\80T,d,e. â¬\86[d, e] T ≡ U →
                      dt ≤ d + e → llpx_sn R d U L1 L2.
 #R #L1 #L2 #U #dt #H elim H -L1 -L2 -U -dt
 [ #L1 #L2 #dt #k #HL12 #X #d #e #H #_ >(lift_inv_sort2 … H) -H /2 width=1 by llpx_sn_sort/
@@ -174,7 +174,7 @@ lemma llpx_sn_ge_up: ∀R,L1,L2,U,dt. llpx_sn R dt U L1 L2 → ∀T,d,e. ⇧[d,
 | #I #L1 #L2 #K1 #K2 #W1 #W2 #dt #i #Hdti #HLK1 #HLK2 #HW1 #HW12 #_ #X #d #e #H #_
   elim (lift_inv_lref2 … H) -H * #Hid #H destruct
   [ lapply (llpx_sn_fwd_length … HW1) -HW1 #HK12
-    lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2)
+    lapply (drop_fwd_length … HLK1) lapply (drop_fwd_length … HLK2)
     normalize in ⊢ (%→%→?); -I -W1 -W2 -dt /3 width=1 by llpx_sn_skip, ylt_inj/
   | /4 width=9 by llpx_sn_lref, yle_inj, le_plus_b/
   ]