proveit.logic.equality.unfold_not_equals
proveit.logic.booleans.negation.negation_contradiction