Erasable : Type -> Prop is inconsistent due to its injectivity
(see erasable_inconsistency.v), so limit it to Set->Prop, and add
-impredicative-set.  Also cope with changes to what zauto can solve.