update in basic_2

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

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 86dc07b45fa41b3723979cb35031ac83b490f35b..72d7a1f4b331262d237ce4863c2348cfdbc22394 100644 (file)
--- 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-.