Two cases. One conclusion.
A offers alternatives. Its introduction rules choose one side; elimination must account for both possibilities without confusing their temporary assumptions.
1. Introduce one alternative
From evidence p of A, orLeft(p, B) establishes A ∨ B. From evidence q of B, orRight(A, q) establishes the same disjunction. The other proposition is an annotation, not evidence: left introduction does not prove B.
This is inclusive or, not exclusive or. Proving one side does not claim that the other is false. The first two disjunction examples in the playground establish A → A ∨ B and B → A ∨ B.
2. Use both cases to reach the same result
Suppose the outer Γ provides evidence of A ∨ B. Check the left branch under Γ plus a fresh assumption a : A. Separately check the right branch under Γ plus b : B. If both establish C, conclude C under Γ alone.
The branches must conclude structurally identical . The annotations must match A and B, and each assumption ID must be fresh in its active scope. The two branch assumptions are discharged by disjunction elimination. Neither branch receives the other’s assumption, and neither assumption escapes the join.
| Part | Available assumptions | Conclusion |
|---|---|---|
| Choice | Γ | A ∨ B |
| Left case | Γ plus a : A | B ∨ A, by right introduction |
| Right case | Γ plus b : B | B ∨ A, by left introduction |
| After cases | Γ only | B ∨ A |
3. Inspect the two routes
Choose Disjunction: commutativity by cases, inspect the , and press Check proof. The trace labels Left case and Right case, shows their temporary assumptions, and records the shared conclusion. Collapse a case to compare it with its sibling.
In Disjunction: two routes to C, the outer context supplies f : A → C and g : B → C. The A branch applies f to a; the B branch applies g to b. Both yield C, proving (A → C) → (B → C) → A ∨ B → C after the outer assumptions are discharged.
4. Why plausible shortcuts fail
Returning A in one branch and B in the other does not establish a common result. Borrowing a from the B branch fails because a is out of scope. Changing an assumption annotation to C cannot create evidence of C. The invalid examples expose each mistake with a diagnostic path.
Even if the choice was built with left introduction, the checks both supplied branches before accepting proof by cases. It stops at the first error, so a rejected trace may show only the part checked so far. This is checking explicit evidence, not running a program that skips the unused branch.
5. Take this with you
One side is enough to introduce a disjunction. Using it requires two separately scoped cases with the same conclusion. The kernel checks the evidence and discharges both temporary assumptions.