proveit.logic.sets.inclusion.unfold_subset_eq
proveit.logic.booleans.implication.to_contraposition