proveit.logic.equality.equals_reversal