Proof of proveit.logic.booleans.in_bool_if_false theorem

import proveit
from proveit import A
from proveit.logic import Not
from proveit.logic.booleans import false_is_bool
theory = proveit.Theory() # the theorem's theory

%proving in_bool_if_false

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

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

%qed # proven via automation

proveit.logic.booleans.in_bool_if_false has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	:
2	axiom		⊢
	proveit.logic.booleans.negation.operand_is_bool
3	instantiation	4, 5	⊢
	:
4	conjecture		⊢
	proveit.logic.booleans.in_bool_if_true
5	assumption		⊢