import proveit
from proveit import A, B
from proveit.logic import Boolean, InSet
from proveit.logic.sets.equivalence import set_equiv_def
theory = proveit.Theory() # the theorem's theory
%proving set_equiv_is_bool
set_equiv_def
set_equiv_def_inst = set_equiv_def.instantiate()
set_equiv_in_bool_as_defined = set_equiv_def_inst.rhs.deduce_in_bool()
set_equiv_def_inst.sub_left_side_into(set_equiv_in_bool_as_defined)
%qed