Let X, Y and z be given.
Assume H1: z ∈ X ∪ Y.
We will prove z ∈ X ∨ z ∈ Y.
Apply (UnionE_impred {X,Y} z H1) to the current goal.
Let Z be given.
Assume H2: z ∈ Z.
Assume H3: Z ∈ {X,Y}.
Apply (UPairE Z X Y H3) to the current goal.
Assume H4: Z = X.
Apply orIL to the current goal.
We will prove z ∈ X.
rewrite the current goal using H4 (from right to left).
We will prove z ∈ Z.
An exact proof term for the current goal is H2.
Assume H4: Z = Y.
Apply orIR to the current goal.
We will prove z ∈ Y.
rewrite the current goal using H4 (from right to left).
We will prove z ∈ Z.
An exact proof term for the current goal is H2.
∎