commit by user lroversi

[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 2605b921c94df6f991d86ceae50123591694b8e3..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
@@ -62,7 +62,7 @@ fact lpx_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx R L1 L
 | #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_
   >commutative_plus normalize #H destruct
 ]
-qed.
+qed-.
 
-lemma ltpr_dropable: ∀R. dropable_dx (lpx R).
-/2 width=5/ qed.
+lemma lpx_dropable: ∀R. dropable_dx (lpx R).
+/2 width=5 by lpx_dropable_aux/ qed.