(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
-(* Properties with sn for uncounted parallel rt-transition for terms ********)
+(* Properties with sn for unbound parallel rt-transition for terms **********)
(* Basic_2A1: was: csx_fpbs_conf *)
lemma fpbs_csx_conf: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →