Let X, Y and z be given.
Assume H1: z ∈ {Inj0 x|x ∈ X} ∪ {Inj1 y|y ∈ Y}.
Apply (binunionE {Inj0 x|x ∈ X} {Inj1 y|y ∈ Y} z H1) to the current goal.
Assume H2: z ∈ {Inj0 x|x ∈ X}.
Apply orIL to the current goal.
An exact proof term for the current goal is (ReplE X Inj0 z H2).
Assume H2: z ∈ {Inj1 y|y ∈ Y}.
Apply orIR to the current goal.
An exact proof term for the current goal is (ReplE Y Inj1 z H2).
∎