notational change of lift, drop, and gget

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gget.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gget.ma
index f299c9beabd8fa1513ad0f0e130f9ba326ee0ccd..acf9602be26d724d701b468fa78cc029837b0b49 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gget.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gget.ma
@@ -28,7 +28,7 @@ interpretation "global reading"
 
 (* basic inversion lemmas ***************************************************)
 
-lemma gget_inv_gt: â\88\80G1,G2,e. â\87©[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
+lemma gget_inv_gt: â\88\80G1,G2,e. â¬\87[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
 #G1 #G2 #e * -G1 -G2 //
 [ #G #H >H -H >commutative_plus #H (**) (* lemma needed here *)
   lapply (le_plus_to_le_r … 0 H) -H #H
@@ -40,7 +40,7 @@ lemma gget_inv_gt: ∀G1,G2,e. ⇩[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
 ]
 qed-.
 
-lemma gget_inv_eq: â\88\80G1,G2,e. â\87©[e] G1 ≡ G2 → |G1| = e + 1 → G1 = G2.
+lemma gget_inv_eq: â\88\80G1,G2,e. â¬\87[e] G1 ≡ G2 → |G1| = e + 1 → G1 = G2.
 #G1 #G2 #e * -G1 -G2 //
 [ #G #H1 #H2 >H2 in H1; -H2 >commutative_plus #H (**) (* lemma needed here *)
   lapply (le_plus_to_le_r … 0 H) -H #H
@@ -51,8 +51,8 @@ lemma gget_inv_eq: ∀G1,G2,e. ⇩[e] G1 ≡ G2 → |G1| = e + 1 → G1 = G2.
 ]
 qed-.
 
-fact gget_inv_lt_aux: â\88\80I,G,G1,G2,V,e. â\87©[e] G ≡ G2 → G = G1. ⓑ{I} V →
-                      e < |G1| â\86\92 â\87©[e] G1 ≡ G2.
+fact gget_inv_lt_aux: â\88\80I,G,G1,G2,V,e. â¬\87[e] G ≡ G2 → G = G1. ⓑ{I} V →
+                      e < |G1| â\86\92 â¬\87[e] G1 ≡ G2.
 #I #G #G1 #G2 #V #e * -G -G2
 [ #G #H1 #H destruct #H2
   lapply (le_to_lt_to_lt … H1 H2) -H1 -H2 normalize in ⊢ (? % ? → ?); >commutative_plus #H
@@ -65,12 +65,12 @@ fact gget_inv_lt_aux: ∀I,G,G1,G2,V,e. ⇩[e] G ≡ G2 → G = G1. ⓑ{I} V →
 qed-.
 
 lemma gget_inv_lt: ∀I,G1,G2,V,e.
-                    â\87©[e] G1. â\93\91{I} V â\89¡ G2 â\86\92 e < |G1| â\86\92 â\87©[e] G1 ≡ G2.
+                    â¬\87[e] G1. â\93\91{I} V â\89¡ G2 â\86\92 e < |G1| â\86\92 â¬\87[e] G1 ≡ G2.
 /2 width=5 by gget_inv_lt_aux/ qed-.
 
 (* Basic properties *********************************************************)
 
-lemma gget_total: â\88\80e,G1. â\88\83G2. â\87©[e] G1 ≡ G2.
+lemma gget_total: â\88\80e,G1. â\88\83G2. â¬\87[e] G1 ≡ G2.
 #e #G1 elim G1 -G1 /3 width=2/
 #I #V #G1 * #G2 #HG12
 elim (lt_or_eq_or_gt e (|G1|)) #He