X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Fgget_gget.ma;h=ee7027ce4d94277d5ca601913174b4d0c651d75e;hb=2ba2dc23443ad764adab652e06d6f5ed10bd912d;hp=6c1001b6af81d070fb76e3ac7c698d382869a596;hpb=29973426e0227ee48368d1c24dc0c17bf2baef77;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/gget_gget.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/gget_gget.ma
index 6c1001b6a..ee7027ce4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/gget_gget.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/gget_gget.ma
@@ -32,7 +32,7 @@ qed-.
 lemma gget_dec: ∀G1,G2,e. Decidable (⇩[e] G1 ≡ G2).
 #G1 #G2 #e
 elim (gget_total e G1) #G #HG1
-elim (genv_eq_dec G G2) #HG2
+elim (eq_genv_dec G G2) #HG2
 [ destruct /2 width=1/
 | @or_intror #HG12
   lapply (gget_mono … HG1 … HG12) -HG1 -HG12 /2 width=1/