proveit.logic.equality.not_equals_contradiction