proveit.logic.equality.rhs_via_equality