proveit.logic.equality.rhs_via_equality
proveit.logic.equality.lhs_via_equality
proveit.logic.sets.inclusion.unfold_subset_eq