Let a and b be given.
Set Y to be the term {a} ∪ {b}.
We prove the intermediate claim HfinY: finite Y.
An exact proof term for the current goal is (binunion_finite {a} (Sing_finite a) {b} (Sing_finite b)).
We prove the intermediate claim Hsub: (UPair a b) ⊆ Y.
Let x be given.
Assume Hx: x ∈ UPair a b.
Apply (UPairE x a b Hx (x ∈ Y)) to the current goal.
Assume Hxa: x = a.
rewrite the current goal using Hxa (from left to right).
An exact proof term for the current goal is (binunionI1 {a} {b} a (SingI a)).
Assume Hxb: x = b.
rewrite the current goal using Hxb (from left to right).
An exact proof term for the current goal is (binunionI2 {a} {b} b (SingI b)).
An exact proof term for the current goal is (Subq_finite Y HfinY (UPair a b) Hsub).
∎