BATs must list sort names; fixed implication and equivalence in proper+ compiler.

* sort_name/2 in BATs must list names of a sort.
* cnf/2 handles negated <-> and -> correctly.
ewff_true() is now (forall x . x = x).

Before, it was (#0 = #0), which led to unnecessarily large setups
because they were instantiated for #0 even if #0 didn't occur in the
setup besides ewff_true().