-lemma fpbs_intro_star: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
- ∀G,L,T0. ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ →
- ∀L0. ⦃G, L⦄ ⊢ ⬈*[h] L0 →
- ∀G2,L2,T2. ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ .
-/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_ffdeq/ qed.
+lemma fpbs_intro_star: ∀h,G1,L1,T1,T. ⦃G1,L1⦄ ⊢ T1 ⬈*[h] T →
+ ∀G,L,T0. ⦃G1,L1,T⦄ ⊐* ⦃G,L,T0⦄ →
+ ∀L0. ⦃G,L⦄ ⊢ ⬈*[h] L0 →
+ ∀G2,L2,T2. ⦃G,L0,T0⦄ ≛ ⦃G2,L2,T2⦄ → ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄ .
+/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_fdeq/ qed.