import proveit
from proveit import defaults
from proveit.logic.sets.equivalence import set_equiv_def
theory = proveit.Theory() # the theorem's theory
%proving set_equiv_unfold
defaults.assumptions = set_equiv_unfold.conditions
set_equiv_def
set_equiv_def.instantiate().derive_right_via_equality()
%qed