let imply a b =
  or_ (not_ a) b