X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbg_fqup.ma;h=c2fde98d7193f721986986d7fac9fcc3a230e07c;hb=adb9ba187619cea977d1d22971eba27eb437cd6a;hp=746aa695379d1a84b61276a50fb48f9a893b6f06;hpb=f677b4ef7fa20f1ab36c5ee59598865d5c1b719b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
index 746aa6953..c2fde98d7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_fqup.ma
@@ -19,9 +19,9 @@ include "basic_2/rt_computation/fpbg.ma".
 
 (* Advanced properties with sort-irrelevant equivalence for terms ***********)
 
-lemma fpbg_tdeq_div: ∀h,G1,G2,L1,L2,T1,T. ⦃G1,L1,T1⦄ >[h] ⦃G2,L2,T⦄ →
+lemma fpbg_teqx_div: ∀h,G1,G2,L1,L2,T1,T. ⦃G1,L1,T1⦄ >[h] ⦃G2,L2,T⦄ →
                      ∀T2. T2 ≛ T → ⦃G1,L1,T1⦄ >[h] ⦃G2,L2,T2⦄.
-/4 width=5 by fpbg_fdeq_trans, tdeq_fdeq, tdeq_sym/ qed-.
+/4 width=5 by fpbg_feqx_trans, teqx_feqx, teqx_sym/ qed-.
 
 (* Properties with plus-iterated structural successor for closures **********)