In [1]:

```
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
```

In [2]:

```
%proving singular_constructive_dilemma
```

In [3]:

```
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.

In [4]:

```
singular_constructive_dilemma_lemma
```

In [5]:

```
singular_constructive_dilemma_lemma.instantiate({C:Equals(C, TRUE)})
```

In [6]:

```
%qed
```

Out[6]: