proveit.logic.sets.inclusion.unfold_proper_subset
proveit.logic.booleans.conjunction.left_from_and
proveit.logic.sets.inclusion.unfold_subset_eq