- lambdadelta: first recursive part of preservation finally proved!

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma
index 61c720754a0103a784e4f7f918ea280d705925c6..27ea45c330b8a697e9bd37625779f64d1798e7db 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma
@@ -35,6 +35,9 @@ lemma fprs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 →
 
 (* Basic properties *********************************************************)
 
+lemma fpr_fprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+/2 width=1/ qed.
+
 lemma fprs_refl: bi_reflexive … fprs.
 /2 width=1/ qed.