see dependencies
import proveit
from proveit.logic import InSet, Equals, Boolean
from proveit import x, y
from proveit.logic.equality import sub_left_side_into
from proveit.logic.sets.enumeration import singleton_def
%proving in_singleton_is_bool
state1 = singleton_def.instantiate({x:x, y:y})
state2 = InSet(Equals(x,y), Boolean).prove()
state1.sub_left_side_into(state2).generalize([x,y])
%qed