- bug fix in the induction for the closure property

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / fpbc_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_lift.ma
index 6236452bb3cd2e6815b2f6a5bf85aa3c6e60bf9b..987258b79a682097ebf40f31c24c3f45fafc016f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_lift.ma
@@ -22,7 +22,7 @@ include "basic_2/reduction/fpbc.ma".
 
 lemma ssta_fpbc: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 →
                 ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
-#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (term_eq_dec T1 T2)
+#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2)
 /3 width=5 by fpbc_cpx, ssta_cpx/ #H destruct
 elim (ssta_inv_refl_pos … HT1 … HT12)
 qed.