Let A and B be given.

Assume H1: exactly1of2 A B.

Apply (exactly1of2_E A B H1 (A ∨ B)) to the current goal.

An exact proof term for the current goal is (λ(HA : A)(_ : ¬ B) ⇒ orIL A B HA).

An exact proof term for the current goal is (λ(_ : ¬ A)(HB : B) ⇒ orIR A B HB).

∎