import proveit
from proveit import defaults
from proveit import A, B, C
from proveit.logic import Implies, Not, Or
theory = proveit.Theory() # the theorem's theory
%proving singular_constructive_dilemma_lemma
defaults.assumptions = singular_constructive_dilemma_lemma.conditions
Implies(A, C).deny_antecedent(assumptions=defaults.assumptions + (Not(C),))
Implies(B, C).deny_antecedent(assumptions=defaults.assumptions + (Not(C),))
Or(A, B).affirm_via_contradiction(C)
%qed