proveit.logic.sets.inclusion.subset_eq_via_equality