-lemma coafter_fwd_at1: â\88\80i,i2,i1,f,f2. @â¦\83i1, fâ¦\84 â\89¡ i â\86\92 @â¦\83i2, f2â¦\84 â\89¡ i →
- â\88\80f1. f2 ~â\8a\9a f1 â\89¡ f â\86\92 @â¦\83i1, f1â¦\84 â\89¡ i2.
+lemma coafter_fwd_at1: â\88\80i,i2,i1,f,f2. @â\9dªi1, fâ\9d« â\89\98 i â\86\92 @â\9dªi2, f2â\9d« â\89\98 i →
+ â\88\80f1. f2 ~â\8a\9a f1 â\89\98 f â\86\92 @â\9dªi1, f1â\9d« â\89\98 i2.