let mk_poslit = function
  | Atom.True -> True
  | Atom.False -> False
  | a -> Atom(a)