see dependencies
import proveit
from proveit import x, S
from proveit.logic.sets.membership import not_in_set_def
theory = proveit.Theory() # the theorem's theory
%proving fold_not_in_set
not_in_set_def
not_in_set_def_spec = not_in_set_def.instantiate({x:x, S:S})
not_in_set_def_spec.derive_left_via_equality(assumptions=[not_in_set_def_spec.rhs])
%qed