In [1]:
import proveit
# we need to import false_or_false_negated to derive it's side-effects:
from proveit.logic.booleans.disjunction import \
    (true_or_true, false_or_true, true_or_false, false_or_false_negated)
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving binary_closure
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
(see dependencies)
binary_closure may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".
In [3]:
proveit.logic.booleans.disjunction.binary_closure has been proven.