update in staic_2 and basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma
index 19aeffac62f3a44351657bbd4539cfe8c681c1b0..14a0f8098fba2a99a67f675ce7b927e0b5ef4ec7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_reqx.ma
@@ -32,7 +32,7 @@ lemma teqx_fpb_trans:
 | #T1 #HUT1 #HnUT1
   lapply (teqx_cpx_trans … HU21 … HUT1) -HUT1
   /6 width=5 by fpb_cpx, teqx_canc_sn, teqx_trans, ex3_2_intro/
-| /6 width=5 by fpb_lpx, rpx_teqx_div, teqx_reqx_conf, ex3_2_intro/
+| /6 width=5 by fpb_lpx, rpx_teqx_div, teqx_reqx_conf_sn, ex3_2_intro/
 ]
 qed-.
 
@@ -45,7 +45,7 @@ lemma reqx_fpb_trans:
 [ #G #L2 #U #H2 elim (reqx_fqu_trans … H2 … HT) -K2
   /3 width=5 by fpb_fqu, ex3_2_intro/
 | #U #HTU #HnTU lapply (reqx_cpx_trans … HT … HTU) -HTU
-  /5 width=11 by fpb_cpx, cpx_reqx_conf_sn, teqx_trans, teqx_reqx_conf, ex3_2_intro/ (**) (* time: 36s on dev *)
+  /5 width=11 by fpb_cpx, cpx_reqx_conf_sn, teqx_trans, teqx_reqx_conf_sn, ex3_2_intro/ (**) (* time: 36s on dev *)
 | #L2 #HKL2 #HnKL2 elim (reqx_lpx_trans … HKL2 … HT) -HKL2
   /6 width=5 by fpb_lpx, (* 2x *) reqx_canc_sn, ex3_2_intro/
 ]