import proveit
from proveit.logic.sets.inclusion import not_proper_subset_def
theory = proveit.Theory() # the theorem's theory
%proving fold_not_proper_subset
# pull in the definition of not proper subset
not_proper_subset_def
not_proper_subset_def_inst = not_proper_subset_def.instantiate()
not_proper_subset_def_inst.derive_left_via_equality(assumptions=[not_proper_subset_def_inst.rhs])
%qed