X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fltprs_ltprs.ma;h=7ededf2afd600fcbd9238753a062494c5724eea5;hb=eb4b3b1b307fc392c36f0be253e6a111553259bc;hp=aec82cd5ae1b30dcec47632d41d5ae11638fb043;hpb=bdff98417627c404aacec8ebb07812287783c500;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma
index aec82cd5a..7ededf2af 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma
@@ -19,7 +19,7 @@ include "basic_2/computation/ltprs.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma ltprs_strip: ∀L1. ∀L:term. L ➡* L1 → ∀L2. L ➡ L2 →
+lemma ltprs_strip: ∀L1. ∀L:lenv. L ➡* L1 → ∀L2. L ➡ L2 →
                    ∃∃L0. L1 ➡ L0 & L2 ➡* L0.
 /3 width=3/ qed.