let mk_cons a b = 
  match a, b with
  (*  | App(Pair(Car), [x]), App(Pair(Cdr), [x'])  
        when Term.eq x x' -> x *)
    | _ ->
        Term.mk_app cons [a;b]