Let A and B be given.

Assume u: ¬ (A ∨ B).

Apply andI to the current goal.

We will prove ¬ A.

Assume a: A.

An exact proof term for the current goal is (u (orIL A B a)).

We will prove ¬ B.

Assume b: B.

An exact proof term for the current goal is (u (orIR A B b)).

∎