Proof of proveit.logic.booleans.forall_over_bool_by_cases theorem

import proveit
from proveit import defaults
from proveit import PofA
from proveit.logic import PofTrue, PofFalse
from proveit.logic.booleans.disjunction import singular_constructive_dilemma
theory = proveit.Theory() # the theorem's theory

%proving forall_over_bool_by_cases

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

defaults.assumptions=forall_over_bool_by_cases.all_conditions()

defaults.assumptions:

Ain_bool=defaults.assumptions[2]

Ain_bool:

ATRUEorFALSE=Ain_bool.unfold()

ATRUEorFALSE:  ⊢  

AequalTRUE, AequalFALSE=ATRUEorFALSE.operands

AequalTRUE:

AequalFALSE:

AequalTRUE.sub_left_side_into(PofTrue, assumptions=defaults.assumptions + (AequalTRUE,))

,  ⊢  

AequalFALSE.sub_left_side_into(PofFalse, assumptions=defaults.assumptions + (AequalFALSE,))

,  ⊢  

ATRUEorFALSE.derive_via_dilemma(PofA)

, ,  ⊢  

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

%qed

proveit.logic.booleans.forall_over_bool_by_cases has been proven.

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