- lambdadelta: first recursive part of preservation finally proved!

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma
index a193f3c0a93ce6623dad2946a41fb58716e147cc..c27e7673bc17bfa810e1356698a7684bf9638c0e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs.ma
@@ -40,6 +40,9 @@ qed-.
 
 (* Basic properties *********************************************************)
 
+lemma lfpr_lfprs: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄.
+/2 width=1/ qed.
+
 lemma lfprs_refl: ∀L. ⦃L⦄ ➡* ⦃L⦄.
 /2 width=1/ qed.