proveit.logic.equality.rhs_via_equality
proveit.logic.booleans.conjunction.left_from_and