update in staic_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / fpb_feqx.ma

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 04989deb0fa126dcdafa7a114277072261d10d43..c0e6a4b510d25d4afe4f5ef24ba8fa1978038df6 100644 (file)
--- 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 **************)