proveit.logic.equality.lhs_via_equality