- commit of the "substitution" component

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lpxs_cpxs.ma

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 10600383a97ccc1a1257208cbb2bf8ffc5127552..c961d137c61ee5f4d37b3adf20e1fdf5f5356968 100644 (file)
--- 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-.