import proveit
from proveit.logic.sets.inclusion import not_subset_eq_def
%proving unfold_not_subset_eq
# Pull in the definition for NotSubsetEq
not_subset_eq_def
not_subset_eq_def_inst = not_subset_eq_def.instantiate()
not_subset_eq_def_inst.derive_right_via_equality(assumptions=[not_subset_eq_def_inst.lhs])
%qed