X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fldrop_lpx.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fldrop_lpx.ma;h=adfbbc0380a349d9544180024a22f2d656e4bb23;hb=6d3e67a714d59ff5d0da7aff72323a6d2ac07db4;hp=f972cb2b2f3d8687ba3ee315ae390944a2ef32e8;hpb=28b55bc982671bad6514751c3a368b6cc6cbeec7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma
index f972cb2b2..adfbbc038 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrop_lpx.ma
@@ -64,5 +64,5 @@ fact lpx_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx R L1 L
 ]
 qed-.
 
-lemma ltpx_dropable: ∀R. dropable_dx (lpx R).
+lemma lpx_dropable: ∀R. dropable_dx (lpx R).
 /2 width=5 by lpx_dropable_aux/ qed.