update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / csx_reqx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma
index f6f8970e3f9740679a8c4c24f45f8714717e9a43..5d35690cc7ef19e42cab29dcd0060a700d838399 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_reqx.ma
@@ -26,8 +26,8 @@ lemma csx_reqx_conf (G) (L1):
 #G #L1 #T #H
 @(csx_ind … H) -T #T1 #_ #IH #L2 #HL12
 @csx_intro #T2 #HT12 #HnT12
-elim (reqx_cpx_trans … HL12 … HT12) -HT12
-/5 width=5 by cpx_reqx_conf_sn, csx_teqx_trans, teqx_trans/
+lapply (reqx_cpx_trans … HL12 … HT12) -HT12
+/3 width=4 by cpx_reqx_conf_sn/
 qed-.
 
 (* Basic_2A1: uses: csx_lleq_trans *)