Proof of proveit.logic.booleans.disjunction.each_is_bool theorem

import proveit
from proveit import defaults
#from proveit import Lambda, Iter, Indexed
from proveit import A, B, C, D, i, j, k, l, m, n
from proveit.logic import Or, TRUE, FALSE, Forall, Implies, Not, in_bool, And, Boolean, Equals, Set
from proveit.core_expr_types import A_1_to_m, C_1_to_n
from proveit.numbers import Natural, NaturalPos, Add, Exp, one, LessEq
from proveit.logic.booleans.disjunction  import left_in_bool, right_in_bool, multi_disjunction_def
theory = proveit.Theory() # the theorem's theory

%proving each_is_bool

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

defaults.assumptions = each_is_bool.all_conditions()

defaults.assumptions:

BeqT_or_BeqF = in_bool(B).unfold(assumptions=[in_bool(B)])

BeqT_or_BeqF:  ⊢  

BeqT = BeqT_or_BeqF.operands[0]

BeqT:

BeqT.evaluation(assumptions=[BeqT])

 ⊢  

BeqF = BeqT_or_BeqF.operands[1]

BeqF:

BeqF.evaluation(assumptions=[BeqF])

 ⊢