X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_csx.ma;h=72d7a1f4b331262d237ce4863c2348cfdbc22394;hp=86dc07b45fa41b3723979cb35031ac83b490f35b;hb=b2cdc4abd9ac87e39bc51b0d9c38daea179adbd5;hpb=3c7b4071a9ac096b02334c1d47468776b948e2de

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma
index 86dc07b45..72d7a1f4b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma
@@ -23,7 +23,8 @@ lemma csx_teqx_trans (G) (L):
       ∀T1. ❪G,L❫ ⊢ ⬈*𝐒 T1 →
       ∀T2. T1 ≛ T2 → ❪G,L❫ ⊢ ⬈*𝐒 T2.
 #G #L #T1 #H @(csx_ind … H) -T1 #T #_ #IH #T2 #HT2
-@csx_intro #T1 #HT21 #HnT21 elim (teqx_cpx_trans … HT2 … HT21) -HT21
+@csx_intro #T1 #HT21 #HnT21
+lapply (teqx_cpx_trans … HT2 … HT21) -HT21 #HT1
 /4 width=5 by teqx_repl/
 qed-.