let d_interp = function
  | Term.App(op, l, _) -> (Sym.Propset.get op, l)
  | _ -> raise Not_found