- lambdadelta: more service lemmas ...

[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 b7b0e1094b8e0b9774744aee6675b3db40fed432..34ad45039e8a407348cdef11a6d7d9299519cc69 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,12 @@ qed-.
 lemma ltprs_refl: reflexive … ltprs.
 /2 width=1/ qed.
 
+lemma ltprs_strap1: ∀L1,L,L2. L1 ➡* L → L ➡ L2 → L1 ➡* L2.
+/2 width=3/ qed.
+
+lemma ltprs_strap2: ∀L1,L,L2. L1 ➡ L → L ➡* L2 → L1 ➡* L2.
+/2 width=3/ qed.
+
 (* Basic inversion lemmas ***************************************************)
 
 lemma ltprs_inv_atom1: ∀L2. ⋆ ➡* L2 → L2 = ⋆.