(*** after_isid_inv_sn *)
lemma pr_after_isi_inv_sn:
- â\88\80f1,f2,f. f1 â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f1â\9d© â\86\92 f2 â\89¡ f.
+ â\88\80f1,f2,f. f1 â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f1â\9d© â\86\92 f2 â\89\90 f.
/3 width=6 by pr_after_isi_sn, pr_after_mono/ qed-.
(*** after_isid_inv_dx *)
lemma pr_after_isi_inv_dx:
- â\88\80f1,f2,f. f1 â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f2â\9d© â\86\92 f1 â\89¡ f.
+ â\88\80f1,f2,f. f1 â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f2â\9d© â\86\92 f1 â\89\90 f.
/3 width=6 by pr_after_isi_dx, pr_after_mono/ qed-.
(*** after_fwd_isid1 *)