lemma fpbs_inv_alt: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
∃∃L0,L,T. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T &
⦃G1, L1, T⦄ ⊐* ⦃G2, L0, T2⦄ &
lemma fpbs_inv_alt: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
∃∃L0,L,T. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T &
⦃G1, L1, T⦄ ⊐* ⦃G2, L0, T2⦄ &