/3 width=1 by fpbc_cpx, cpr_cpx/ qed.
(* Inversion lemmas on "big tree" parallel reduction for closures ***********)
lemma fpb_inv_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →
/3 width=1 by fpbc_cpx, cpr_cpx/ qed.
(* Inversion lemmas on "big tree" parallel reduction for closures ***********)
lemma fpb_inv_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ →