X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Fgdrop_gdrop.ma;h=640c36c7802ec97fab7f6c0074a34e1a4ffa98cc;hb=fcd30dfead2fbc2889aa993fba0577dce8a90c88;hp=9083e2b3a028827f069d41222eb775556d5c4715;hpb=b5a168bec5e813258c510a1f2a00ce9f57ecee5a;p=helm.git

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 9083e2b3a..640c36c78 100644
--- 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: ∀G,G1,e. ⇓[e] G ≡ G1 → ∀G2. ⇓[e] G ≡ G2 → G1 = G2.
+theorem gdrop_mono: ∀G,G1,e. ⇩[e] G ≡ G1 → ∀G2. ⇩[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: ∀G1,G2,e. Decidable (⇓[e] G1 ≡ G2).
+lemma gdrop_dec: ∀G1,G2,e. Decidable (⇩[e] G1 ≡ G2).
 #G1 #G2 #e
 elim (gdrop_total e G1) #G #HG1
 elim (genv_eq_dec G G2) #HG2