proveit.logic.equality.rhs_via_equality
proveit.logic.equality.substitute_in_true