let sym_d_uninterp = function 
  | Uninterp(n) -> n 
  | _ -> assert false