(* Constructions with pr_tl *************************************************)
(*** isid_tl *)
-lemma pr_isi_tl (f): ð\9d\90\88â\9dªfâ\9d« â\86\92 ð\9d\90\88â\9dªâ«°fâ\9d«.
+lemma pr_isi_tl (f): ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90\88â\9d¨â«°fâ\9d©.
#f cases (pr_map_split_tl f) * #H
[ /2 width=3 by pr_isi_inv_push/
| elim (pr_isi_inv_next … H) -H //