-lemma fpbs_intro_star: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
- â\88\80G,L,T0. â¦\83G1, L1, Tâ¦\84 â\8a\90* â¦\83G, L, T0â¦\84 →
- â\88\80L0. â¦\83G, Lâ¦\84 ⊢ ⬈*[h] L0 →
- â\88\80G2,L2,T2. â¦\83G, L0, T0â¦\84 â\89\9b[h, o] â¦\83G2, L2, T2â¦\84 â\86\92 â¦\83G1, L1, T1â¦\84 â\89¥[h, o] â¦\83G2, L2, T2â¦\84 .
-/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_fdeq/ qed.
+lemma fpbs_intro_star: ∀h,G1,L1,T1,T. ❪G1,L1❫ ⊢ T1 ⬈*[h] T →
+ â\88\80G,L,T0. â\9dªG1,L1,Tâ\9d« â¬\82* â\9dªG,L,T0â\9d« →
+ â\88\80L0. â\9dªG,Lâ\9d« ⊢ ⬈*[h] L0 →
+ â\88\80G2,L2,T2. â\9dªG,L0,T0â\9d« â\89\9b â\9dªG2,L2,T2â\9d« â\86\92 â\9dªG1,L1,T1â\9d« â\89¥[h] â\9dªG2,L2,T2â\9d« .
+/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_feqx/ qed.