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_fold
defaults.assumptions = set_equiv_fold.conditions
set_equiv_def
set_equiv_def.instantiate().derive_left_via_equality()
%qed