proveit.logic.equality.sub_right_side_into