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