- a reinforement in a lemma on ldrop allows to prove a lemma on lsx :)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cpx_cpys.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma
index fa1d4e8d242a0a912440029f38a2b36450efa6fd..3b38ee6abec80be3222d5b904606b21ccf4668fd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma
@@ -24,7 +24,7 @@ lemma lsuby_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) (lsuby 0 (∞)).
 [ //
 | /2 width=2 by cpx_sort/
 | #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/
+  elim (lsuby_ldrop_trans_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/
 |4,9: /4 width=1 by cpx_bind, cpx_beta, lsuby_pair_O_Y/
 |5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/
 |6,10: /4 width=3 by cpx_zeta, cpx_theta, lsuby_pair_O_Y/