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