see dependencies
import proveit
from proveit import n, x, y
from proveit.numbers import one
from proveit.numbers.numerals.decimals import nat1
from proveit.logic.booleans.disjunction import unary_or_reduction
from proveit.logic.sets.enumeration import enum_set_def
%proving singleton_def
enum_set_def
enum_set_def.instantiate({n:one, x:x, y:[y]})
%qed