Let X, Y, z and p be given.

Assume H1 H2 Hz.

Apply binunionE X Y z Hz to the current goal.

Assume H3: z ∈ X.

An exact proof term for the current goal is H1 H3.

Assume H3: z ∈ Y.

An exact proof term for the current goal is H2 H3.

∎