Proof of proveit.logic.booleans.unfold_is_bool theorem

import proveit
from proveit import defaults
from proveit import A
from proveit.logic.booleans import unfold_is_bool_explicit
from proveit.logic.booleans.negation import closure
neg_closure = closure
from proveit.logic.booleans.disjunction import constructive_dilemma
theory = proveit.Theory() # the theorem's theory

%proving unfold_is_bool

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

defaults.assumptions = unfold_is_bool.conditions

defaults.assumptions:

unfold_is_bool_explicit

 ⊢  

explicit_form = unfold_is_bool_explicit.instantiate({A:A})

explicit_form:  ⊢  

explicit_form.derive_via_multi_dilemma(unfold_is_bool.instance_expr)

 ⊢  

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

%qed

proveit.logic.booleans.unfold_is_bool has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4, 21, 5, 15, 6, 7	⊢
	: , : , : , :
2	conjecture		⊢
	proveit.logic.booleans.disjunction.constructive_dilemma
3	instantiation	8, 10	⊢
	: , :
4	instantiation	9, 10	⊢
	: , :
5	instantiation	11, 21	⊢
	:
6	deduction	12	⊢
7	deduction	13	⊢
8	axiom		⊢
	proveit.logic.booleans.disjunction.left_in_bool
9	axiom		⊢
	proveit.logic.booleans.disjunction.right_in_bool
10	instantiation	14, 15	⊢
	:
11	conjecture		⊢
	proveit.logic.booleans.negation.closure
12	instantiation	16, 17	⊢
	:
13	instantiation	18, 19	⊢
	:
14	conjecture		⊢
	proveit.logic.booleans.in_bool_if_true
15	instantiation	20, 21	⊢
	:
16	axiom		⊢
	proveit.logic.booleans.eq_true_elim
17	assumption		⊢
18	theorem		⊢
	proveit.logic.booleans.negation.negation_intro
19	assumption		⊢
20	conjecture		⊢
	proveit.logic.booleans.unfold_is_bool_explicit
21	assumption		⊢