see dependencies
import proveit
from proveit import defaults
from proveit import x, y
from proveit.logic import NotEquals, Not, Equals, TRUE, FALSE, InSet, NotInSet, Set
from proveit.logic.equality import not_equals_def
from proveit.logic.equality import sub_right_side_into
from proveit.logic.sets.enumeration import not_in_singleton_equiv, in_singleton_eval_true, singleton_def
%proving in_singleton_eval_false
defaults.assumptions = in_singleton_eval_false.conditions
step1 = not_equals_def.instantiate({x:x, y:y})
state1 = Equals(NotEquals(x,y), TRUE).prove()
step1.sub_right_side_into(state1)
state2 = Equals(Equals(x,y), FALSE).prove()
state3 = singleton_def.instantiate({x:x, y:y})
goal = state3.sub_left_side_into(state2)
goal.generalize([x,y], conditions = in_singleton_eval_false.conditions)
%qed