import proveit
from proveit import defaults
from proveit import A, B
from proveit.logic.booleans.disjunction import neither_intro
from proveit.logic.booleans.negation import negation_contradiction
theory = proveit.Theory() # the theorem's theory
%proving binary_or_contradiction
defaults.assumptions = binary_or_contradiction.conditions
neither_intro
neither = neither_intro.instantiate({A:A, B:B})
neither.derive_contradiction()
%qed