# import sys
# sys.path.append('..') # allows access to modules in parent theory
import proveit
from proveit.logic.sets.inclusion import not_subset_eq_def
%proving fold_not_subset_eq
# Pull in the definition of NotSubsetEq
not_subset_eq_def
not_subset_eq_def_inst = not_subset_eq_def.instantiate()
not_subset_eq_def_inst.derive_left_via_equality(assumptions=[not_subset_eq_def_inst.rhs])
%qed