Let A and B be given.

Assume H1: exactly1of2 A B.

Let p be given.

Assume H2: A → ¬ B → p.

Assume H3: ¬ A → B → p.

Apply (H1 p) to the current goal.

An exact proof term for the current goal is (λH4 : A ∧ ¬ B ⇒ H4 p H2).

An exact proof term for the current goal is (λH4 : ¬ A ∧ B ⇒ H4 p H3).

∎