-lemma fpbs_intro_star: â\88\80h,G1,L1,T1,T. â¦\83G1,L1â¦\84 ⊢ T1 ⬈*[h] T →
- â\88\80G,L,T0. â¦\83G1,L1,Tâ¦\84 â¬\82* â¦\83G,L,T0â¦\84 →
- â\88\80L0. â¦\83G,Lâ¦\84 ⊢ ⬈*[h] L0 →
- â\88\80G2,L2,T2. â¦\83G,L0,T0â¦\84 â\89\9b â¦\83G2,L2,T2â¦\84 â\86\92 â¦\83G1,L1,T1â¦\84 â\89¥[h] â¦\83G2,L2,T2â¦\84 .
-/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_fdeq/ qed.
+lemma fpbs_intro_star: â\88\80h,G1,L1,T1,T. â\9dªG1,L1â\9d« ⊢ 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.