-lemma cpxs_fpbg_trans (h) (o): ∀G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
- ∀G2,L2,T2. ⦃G1, L1, T⦄ >[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
+lemma cpxs_fpbg_trans (h): ∀G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
+ ∀G2,L2,T2. ⦃G1, L1, T⦄ >[h] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h] ⦃G2, L2, T2⦄.