X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flprs_cprs.ma;h=46c7d1250aea238588cec2612ce83f5b35c03f97;hb=52e675f555f559c047d5449db7fc89a51b977d35;hp=1bcb46d37e387513b586c24bdd4960c5febfd496;hpb=75fac6d60f67a4dfa38ea6c2cc45a18eda5d8996;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma
index 1bcb46d37..46c7d1250 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma
@@ -131,7 +131,7 @@ lemma cprs_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡* U2 →
   ]
 | #U1 #HTU1 #HU01 elim (lift_total U2 0 1)
   #U #HU2 lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0
-  /4 width=3 by cprs_strap1, ldrop_drop, ex3_intro, or_intror/
+  /4 width=3 by cprs_strap1, drop_drop, ex3_intro, or_intror/
 ]
 qed-.