let
equivalent a b =
and_ (imply a b) (imply b a)