X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Ffpbc_lift.ma;h=987258b79a682097ebf40f31c24c3f45fafc016f;hb=02df4ecb9d5ad173a3e306952cc09d83b62cfdcf;hp=6236452bb3cd2e6815b2f6a5bf85aa3c6e60bf9b;hpb=7a112c2797e15ccd67bcbd7308fddcc54bff60ed;p=helm.git

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 6236452bb..987258b79 100644
--- 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.