- new component for restricted computation (delta, zeta and tau only)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / ldrop_lpx.ma

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 f972cb2b2f3d8687ba3ee315ae390944a2ef32e8..adfbbc0380a349d9544180024a22f2d656e4bb23 100644 (file)
--- 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.