- lambdadelta: more service lemmas ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reducibility / lfpr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma
index 5e1ba79926c492ea5f353bb1e9270edaa30bfb58..44745490eb99e8a3f108abc841ce78310a6814ce 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/lfpr.ma
@@ -34,6 +34,9 @@ lemma lfpr_refl: ∀L. ⦃L⦄ ➡ ⦃L⦄.
 lemma ltpss_sn_lfpr: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → ⦃L1⦄ ➡ ⦃L2⦄.
 /3 width=5/ qed.
 
+lemma ltpr_lfpr: ∀L1,L2. L1 ➡ L2 → ⦃L1⦄ ➡ ⦃L2⦄.
+/3 width=3/ qed.
+
 (* Basic inversion lemmas ***************************************************)
 
 lemma lfpr_inv_atom1: ∀L2. ⦃⋆⦄ ➡ ⦃L2⦄ → L2 = ⋆.