X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Funfold%2Fltpss.ma;h=eb7803efe9631f72c282720ea9076685596aef24;hb=035e3f52f8da3cb3cdb493aa20568ad673cc2cf5;hp=e63dbb9a4380600a8ab4fabce165939d332f6be2;hpb=78f21d7d9014e5c7655f58239e4f1a128ea2c558;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma
index e63dbb9a4..eb7803efe 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma
@@ -63,7 +63,7 @@ fact ltps_inv_atom2_aux: ∀d,e,L1,L2.
 ]
 qed.
 
-lemma drop_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆.
+lemma ldrop_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆.
 /2 width=5/ qed.
 
 fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e →