- lambdadelta: first recursive part of preservation finally proved!

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma
index 34ad45039e8a407348cdef11a6d7d9299519cc69..8e0c32e2604c8073093391bc049c87e8e3f34923 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs.ma
@@ -44,6 +44,9 @@ qed-.
 lemma ltprs_refl: reflexive … ltprs.
 /2 width=1/ qed.
 
+lemma ltpr_ltprs: ∀L1,L2. L1 ➡ L2 → L1 ➡* L2.
+/2 width=1/ qed.
+
 lemma ltprs_strap1: ∀L1,L,L2. L1 ➡* L → L ➡ L2 → L1 ➡* L2.
 /2 width=3/ qed.