import proveit
from proveit.logic.sets.equivalence import set_not_equiv_def
theory = proveit.Theory() # the theorem's theory
%proving set_not_equiv_is_bool
set_not_equiv_def
set_not_equiv_def_inst = set_not_equiv_def.instantiate()
negation_in_bool = set_not_equiv_def_inst.rhs.deduce_in_bool()
set_not_equiv_def_inst.sub_left_side_into(negation_in_bool)
%qed