Proof of proveit.logic.booleans.true_is_bool theorem

import proveit
from proveit import A
from proveit.logic import TRUE, FALSE, Or, Equals
from proveit.logic.booleans import fold_is_bool
from proveit.logic.booleans.disjunction import true_or_false
from proveit.logic.equality import unfold_not_equals, sub_left_side_into
theory = proveit.Theory() # the theorem's theory

%proving true_is_bool

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

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

fold_is_bool

 ⊢  

TeqT = Equals(TRUE, TRUE).prove()

TeqT:  ⊢  

not_TeqF = Equals(TRUE, FALSE).disprove()

not_TeqF:  ⊢  

true_or_false

 ⊢  

TeqT_or_F = true_or_false.inner_expr().operands[0].substitute(TeqT.expr)

TeqT_or_F:  ⊢  

TeqT_or_F.inner_expr().operands[1].substitute(not_TeqF.operand, auto_simplify=False)

 ⊢  

fold_is_bool.instantiate({A:TRUE})

 ⊢  

%qed

proveit.logic.booleans.true_is_bool has been proven.

	step type	requirements	statement
0	instantiation	1, 2	⊢
	:
1	conjecture		⊢
	proveit.logic.booleans.fold_is_bool
2	instantiation	3, 4, 5	⊢
	: , :
3	theorem		⊢
	proveit.logic.equality.substitute_falsehood
4	instantiation	6, 7, 8	⊢
	: , :
5	instantiation	9, 10	⊢
	: , :
6	theorem		⊢
	proveit.logic.equality.substitute_truth
7	theorem		⊢
	proveit.logic.booleans.disjunction.true_or_false
8	theorem		⊢
	proveit.logic.booleans.true_eq_true
9	theorem		⊢
	proveit.logic.equality.unfold_not_equals
10	theorem		⊢
	proveit.logic.booleans.true_not_false