lemma fqup_cpms_fwd_fpbg (h) (o): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T⦄ →
∀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 fqup_cpms_fwd_fpbg (h) (o): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T⦄ →
∀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-.