(*** coafter_isuni_isid *)
lemma pr_coafter_isu_isi:
- â\88\80f2. ð\9d\90\88â\9dªf2â\9d« â\86\92 â\88\80f1. ð\9d\90\94â\9dªf1â\9d« → f1 ~⊚ f2 ≘ f2.
+ â\88\80f2. ð\9d\90\88â\9d¨f2â\9d© â\86\92 â\88\80f1. ð\9d\90\94â\9d¨f1â\9d© → f1 ~⊚ f2 ≘ f2.
#f #Hf #g #H
elim (pr_isu_inv_uni … H) -H #n #H
/5 width=4 by pr_isi_pushs, pr_isi_inv_eq_repl, pr_coafter_eq_repl_back, pr_coafter_eq_repl_back_sn/