X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Ffprs.ma;h=27ea45c330b8a697e9bd37625779f64d1798e7db;hb=7abd5e0412171f7d07e085d334198c034895c2c3;hp=61c720754a0103a784e4f7f918ea280d705925c6;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fprs.ma
index 61c720754..27ea45c33 100644
--- 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.