proveit.logic.sets.inclusion.fold_subset_eq