qed.
lemma pr_after_uni_isi_next (h1):
- â\88\80f2. ð\9d\90\88â\9dªf2â\9d« → 𝐮❨h1❩ ⊚ ↑f2 ≘ ↑𝐮❨h1❩.
+ â\88\80f2. ð\9d\90\88â\9d¨f2â\9d© → 𝐮❨h1❩ ⊚ ↑f2 ≘ ↑𝐮❨h1❩.
#h1 @(nat_ind_succ … h1) -h1
/5 width=7 by pr_after_isi_dx, pr_after_eq_repl_back_sn, pr_after_next, pr_after_push, pr_isi_inv_eq_push/
qed.