- parallel substitution reaxiomatized

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / ltprs_ltprs.ma

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 aec82cd5ae1b30dcec47632d41d5ae11638fb043..7ededf2afd600fcbd9238753a062494c5724eea5 100644 (file)
--- 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.