- notation restyling ...

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / substitution / gdrop_gdrop.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop_gdrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop_gdrop.ma
index 9083e2b3a028827f069d41222eb775556d5c4715..640c36c7802ec97fab7f6c0074a34e1a4ffa98cc 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop_gdrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop_gdrop.ma
@@ -18,7 +18,7 @@ include "Basic_2/substitution/gdrop.ma".
 
 (* Main properties **********************************************************)
 
-theorem gdrop_mono: â\88\80G,G1,e. â\87\93[e] G â\89¡ G1 â\86\92 â\88\80G2. â\87\93[e] G ≡ G2 → G1 = G2.
+theorem gdrop_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
   >(gdrop_inv_gt … H He) -H -He //
@@ -29,7 +29,7 @@ theorem gdrop_mono: ∀G,G1,e. ⇓[e] G ≡ G1 → ∀G2. ⇓[e] G ≡ G2 → G1
 ]
 qed-.
 
-lemma gdrop_dec: â\88\80G1,G2,e. Decidable (â\87\93[e] G1 ≡ G2).
+lemma gdrop_dec: â\88\80G1,G2,e. Decidable (â\87©[e] G1 ≡ G2).
 #G1 #G2 #e
 elim (gdrop_total e G1) #G #HG1
 elim (genv_eq_dec G G2) #HG2