import proveit
from proveit.logic.booleans import true_is_bool, false_is_bool, in_bool_if_true
from proveit.logic.booleans.conjunction import and_if_both
from proveit.logic.booleans.negation import not_f, not_t
from proveit.logic.equality import substitute_truth
from proveit import defaults
in_bool_if_true.proof().disable(); substitute_truth.proof().disable() # force a more short, symmetric proof
theory = proveit.Theory() # the theorem's theory
%proving closure
true_is_bool
not_f
not_f.sub_left_side_into(true_is_bool)
false_is_bool
not_t
not_t.sub_left_side_into(false_is_bool)
%qed