Proof of proveit.logic.booleans.conditioned_forall_over_bool_by_cases theorem

import proveit
from proveit import defaults
from proveit.logic import Implies, Forall, Boolean
from proveit import PofA, QofA, P, A, Q
from proveit.logic import QimplPofTrue, QimplPofFalse, PofTrue, PofFalse
from proveit.logic.booleans import forall_over_bool_by_cases
theory = proveit.Theory() # the theorem's theory

%proving conditioned_forall_over_bool_by_cases

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

defaults.assumptions = (conditioned_forall_over_bool_by_cases.conditions + 
                        conditioned_forall_over_bool_by_cases.instance_expr.conditions)

defaults.assumptions:

forall_over_bool_by_cases

 ⊢  

forall_over_bool_by_cases_spec = forall_over_bool_by_cases.instantiate({PofA:Implies(QofA,PofA)})

forall_over_bool_by_cases_spec: ,  ⊢  

QAimplPA = forall_over_bool_by_cases_spec.generalize((P, Q), conditions=forall_over_bool_by_cases_spec.assumptions)

QAimplPA:  ⊢  

QAimplPA.instantiate({P:P, Q:Q, A:A})

, ,  ⊢  

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

%qed

proveit.logic.booleans.conditioned_forall_over_bool_by_cases has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	modus ponens	2, 3	, , ,  ⊢
2	instantiation	4, 5	, ,  ⊢
	:
3	assumption		⊢
4	instantiation	6, 7, 8	,  ⊢
	:
5	assumption		⊢
6	conjecture		⊢
	proveit.logic.booleans.forall_over_bool_by_cases
7	assumption		⊢
8	assumption		⊢