import proveit
from proveit import defaults
from proveit import C
from proveit.logic import TRUE, Equals
from proveit.logic.booleans.disjunction import singular_constructive_dilemma_lemma
theory = proveit.Theory() # the theorem's theory
%proving singular_constructive_dilemma
defaults.assumptions = singular_constructive_dilemma.all_conditions()
We will use the constrained singular constructive dilemma as a convenient Lemma to prove some $C=\top$ and deriving $C$ from there.
singular_constructive_dilemma_lemma
singular_constructive_dilemma_lemma.instantiate({C:Equals(C, TRUE)})
%qed