Let A and B be given.

Assume HA: A.

Assume HB: ¬ B.

We will prove A ∧ ¬ B ∨ ¬ A ∧ B.

Apply orIL to the current goal.

We will prove A ∧ ¬ B.

An exact proof term for the current goal is (andI A (¬ B) HA HB).

∎