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().