X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpms_fpbg.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpms_fpbg.ma;h=ea81fda63064b3edb93c7029293187503f983fd3;hb=b98ec1a1a37602eca524dc5487c357a200bbb5b6;hp=7e40bcc6c0b52954e3557a108ba33a018be16319;hpb=eeeaecfafd5ddffa54a41356104fbc60369e5d73;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma
index 7e40bcc6c..ea81fda63 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_fpbg.ma
@@ -24,6 +24,10 @@ lemma fqup_cpms_fwd_fpbg (h) (o): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ⊐+ ⦃
                                   ∀n,T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
 /3 width=5 by cpms_fwd_fpbs, fqup_fpbg,fpbg_fpbs_trans/ qed-.
 
+lemma fpbg_cpms_trans (h) (o) (n): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T⦄ →
+                                   ∀T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
+/3 width=5 by fpbg_fpbs_trans, cpms_fwd_fpbs/ qed-.
+
 lemma cpms_fpbg_trans (h) (o) (n): ∀G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ➡*[n,h] T →
                                    ∀G2,L2,T2. ⦃G1, L1, T⦄ >[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
 /3 width=5 by fpbs_fpbg_trans, cpms_fwd_fpbs/ qed-.