proveit.logic.sets.equivalence.unfold_set_not_equiv
proveit.logic.booleans.negation.negation_contradiction