notational change of lift, drop, and gget

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gget_gget.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gget_gget.ma
index 2f75c9812412772f8feb72c702c892c7aa5632e9..bf14f9e44877c5f9cf97201f9ea71ea7c102e13e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gget_gget.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gget_gget.ma
@@ -18,7 +18,7 @@ include "basic_2/substitution/gget.ma".
 
 (* Main properties **********************************************************)
 
-theorem gget_mono: â\88\80G,G1,e. â\87©[e] G â\89¡ G1 â\86\92 â\88\80G2. â\87©[e] G ≡ G2 → G1 = G2.
+theorem gget_mono: â\88\80G,G1,e. â¬\87[e] G â\89¡ G1 â\86\92 â\88\80G2. â¬\87[e] G ≡ G2 → G1 = G2.
 #G #G1 #e #H elim H -G -G1
 [ #G #He #G2 #H
   >(gget_inv_gt … H He) -H -He //
@@ -29,7 +29,7 @@ theorem gget_mono: ∀G,G1,e. ⇩[e] G ≡ G1 → ∀G2. ⇩[e] G ≡ G2 → G1
 ]
 qed-.
 
-lemma gget_dec: â\88\80G1,G2,e. Decidable (â\87©[e] G1 ≡ G2).
+lemma gget_dec: â\88\80G1,G2,e. Decidable (â¬\87[e] G1 ≡ G2).
 #G1 #G2 #e
 elim (gget_total e G1) #G #HG1
 elim (eq_genv_dec G G2) #HG2