import proveit
from proveit.logic.sets.equivalence import set_not_equiv_def
theory = proveit.Theory() # the theorem's theory
%proving unfold_set_not_equiv
set_not_equiv_def
set_not_equiv_def_inst = set_not_equiv_def.instantiate()
set_not_equiv_def_inst.derive_right_via_equality(assumptions=[set_not_equiv_def_inst.lhs])
%qed