proveit.logic.equality.sub_left_side_into
proveit.logic.equality.equals_reversal