X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flpxs_cpxs.ma;h=c961d137c61ee5f4d37b3adf20e1fdf5f5356968;hb=e5378812c068074f0ac627541d3f066e135c8824;hp=10600383a97ccc1a1257208cbb2bf8ffc5127552;hpb=928cfe1ebf2fbd31731c8851cdec70802596016d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
index 10600383a..c961d137c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
@@ -77,7 +77,7 @@ lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h,
   ]
 | #U1 #HTU1 #HU01
   elim (lift_total U2 0 1) #U #HU2
-  /6 width=11 by cpxs_strap1, cpx_lift, ldrop_ldrop, ex3_intro, or_intror/
+  /6 width=11 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/
 ]
 qed-.