let d_uninterp a =
  assert(is_uninterp a);
  let f,l = Term.destruct a in
  (f, l)