(((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)))
((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))
(((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))
(((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))
((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))














let fancy_of_term : nf -> Console.fancyobj =
  let open Console in
  let of_var level n =
    if n < level
    then fancy_of_string (string_of_var n)
    else (("x" ^ string_of_int (level-n-1)) / ("var<sup>" ^ string_of_int (n-level) ^ "</sup>"))
  in let rec aux level = function
    `Var n -> of_var level n
  | `N n -> fancy_of_string (string_of_int n)
  | `Match(t,bs_lift,bs,args) ->
     "([" ^^ aux level (t :> nf) ^^
     " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (lift bs_lift t)) !bs) ^ "] " ^
     String.concat " " (List.map (print ~l) args) ^ ")"
  | `I(n,args) -> "(" ^ print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")"
  | `Lam nf ->
     let name = string_of_var (List.length l) in
     "λ" ^ name ^ "." ^ print ~l:(name::l) (nf : nf)
  in aux 0
;;