X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Ffpb_feqx.ma;h=c0e6a4b510d25d4afe4f5ef24ba8fa1978038df6;hp=04989deb0fa126dcdafa7a114277072261d10d43;hb=647504aa72b84eb49be8177b88a9254174e84d4b;hpb=b2cdc4abd9ac87e39bc51b0d9c38daea179adbd5

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqx.ma
index 04989deb0..c0e6a4b51 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_feqx.ma
@@ -30,7 +30,7 @@ lemma feqx_fpb_trans:
 elim (teqx_fpb_trans … HT12 … H12) -T2 #K0 #T0 #H #HT0 #HK0
 elim (reqx_fpb_trans … HK12 … H) -K2 #L0 #U0 #H #HUT0 #HLK0
 @(ex2_3_intro … H) -H (**) (* full auto too slow *)
-/4 width=3 by feqx_intro_dx, reqx_trans, teqx_reqx_conf, teqx_trans/
+/4 width=3 by feqx_intro_dx, reqx_trans, teqx_reqx_conf_sn, teqx_trans/
 qed-.
 
 (* Inversion lemmas with degree-based equivalence for closures **************)