- bug fix in the induction for the closure property

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

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 6c1001b6af81d070fb76e3ac7c698d382869a596..ee7027ce4d94277d5ca601913174b4d0c651d75e 100644 (file)
--- 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/