(* Constructions with gr_tl *************************************************)
(*** isfin_tl *)
-lemma gr_isf_tl (f): ð\9d\90\85â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªâ«±f❫.
+lemma gr_isf_tl (f): ð\9d\90\85â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªâ«°f❫.
#f elim (gr_map_split_tl f) * #Hf
/3 width=3 by gr_isf_inv_push, gr_isf_inv_next/
qed.
(* Inversions with gr_tl ****************************************************)
(*** isfin_inv_tl *)
-lemma gr_isf_inv_tl (g): ð\9d\90\85â\9dªâ«±g❫ → 𝐅❪g❫.
+lemma gr_isf_inv_tl (g): ð\9d\90\85â\9dªâ«°g❫ → 𝐅❪g❫.
#f elim (gr_map_split_tl f) * #Hf
/2 width=1 by gr_isf_next, gr_isf_push/
qed-.