see dependencies
import proveit
from proveit import defaults
from proveit import x, y
from proveit.logic import Equals, TRUE
from proveit.logic.sets.enumeration import singleton_def
%proving in_singleton_eval_true
defaults.assumptions = in_singleton_eval_true.conditions
state1 = Equals(Equals(x,y), TRUE).prove()
state2 = singleton_def.instantiate({x:x, y:y}, auto_simplify=False)
goal = state2.sub_left_side_into(state1)
%qed