Proof of proveit.numbers.number_sets.natural_numbers.nat_membership_is_bool theorem

import proveit
from proveit import k, l, n, x
from proveit.numbers import Natural, NaturalPos
from proveit.numbers import zero, one
from proveit.logic import InSet
#from proveit.numbers.number_sets.integers  import naturals_def
#from proveit.numbers.numerals.decimals import posnat1
from proveit.logic.booleans.quantification.universality  import forall_in_bool
theory = proveit.Theory() # the theorem's theory

Must be updated to use Peano's axioms

%proving nat_membership_is_bool

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
nat_membership_is_bool:
(see dependencies)

nat_membership_is_bool may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

# naturals_def

# naturals_def_inst = naturals_def.instantiate({n:x, x:k})

# naturals_def_inst_rhs = naturals_def_inst.rhs

# naturals_def_inst_rhs__inbool = naturals_def_inst_rhs.deduce_in_bool()

# naturals_def_inst.sub_left_side_into(naturals_def_inst_rhs__inbool)

# %qed