F.fprintf frm "\\Intro{%a}{%a}" xx r xl l
| T.LetIn (r, v, _) :: l ->
F.fprintf frm "\\Pose{%a}{%a}{%a}" xx r xat v xl l
+ | T.LApply (r, v, _) :: l ->
+ F.fprintf frm "\\LApply{%a}{%a}{%a}" xx r xat v xl l
| T.Change (u, _, None, _, _) :: l ->
F.fprintf frm "\\Change{%a}{}{%a}" xat u xl l
| T.Change (u, _, Some (s, _), _, _) :: l ->
F.fprintf frm "\\Elim{%a}{%a}{}{}{%a}" xat v xat t xl l
| T.Cut (r, w, _) :: T.Branch ([l1; [T.Id _]], _) :: l2 ->
F.fprintf frm "\\Cut{%a}{%a}{%a}{%a}" xx r xat w xl l1 xl l2
+ | T.Record _ :: _ -> assert false
| T.Inductive _ :: _ -> assert false
| T.Id _ :: _ -> assert false
| T.Clear _ :: _ -> assert false