/3 width=5 by fpbs_fqus_trans, cpxs_fpbs/ qed.
(* Properties with plus-iterated structural successor for closures **********)
lemma cpxs_fqup_fpbs: ∀h,G1,L1,T1,T. ⦃G1,L1⦄ ⊢ T1 ⬈*[h] T →
/3 width=5 by fpbs_fqus_trans, cpxs_fpbs/ qed.
(* Properties with plus-iterated structural successor for closures **********)
lemma cpxs_fqup_fpbs: ∀h,G1,L1,T1,T. ⦃G1,L1⦄ ⊢ T1 ⬈*[h] T →