import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults
from proveit.logic import Implies
from proveit.logic.sets.comprehension import comprehension_def
%proving unfold
defaults.assumptions = unfold.conditions
comprehension_def
comprehension_def_inst = comprehension_def.instantiate().instantiate()
exists_eq_impl = Implies(comprehension_def_inst.rhs, comprehension_def_inst.rhs).prove()
exists_eq_impl.inner_expr().lhs.substitute(comprehension_def_inst.derive_reversed())
%qed