Let A and B be given.

Assume HA: ¬ A.

Assume HB: B.

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

Apply orIR to the current goal.

We will prove ¬ A ∧ B.

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

∎