let mk_cdr = function
  | App(Pair(Cons), [_; b]) -> b
  | a -> Term.mk_app cdr [a]