Let U be given.

Assume HU: U ∈ top_abc_3.

We will prove U ∈ top_abc_9.

Apply (binunionE' (UPair Empty {a_elt}) {abc_set} U (U ∈ top_abc_9)) to the current goal.

Assume HU0: U ∈ UPair Empty {a_elt}.

An exact proof term for the current goal is (binunionI1 (UPair Empty {a_elt} ∪ {UPair a_elt b_elt}) {abc_set} U (binunionI1 (UPair Empty {a_elt}) {UPair a_elt b_elt} U HU0)).

Assume HU0: U ∈ {abc_set}.

We prove the intermediate claim HUeq: U = abc_set.

An exact proof term for the current goal is (SingE abc_set U HU0).

rewrite the current goal using HUeq (from left to right).

An exact proof term for the current goal is (binunionI2 (UPair Empty {a_elt} ∪ {UPair a_elt b_elt}) {abc_set} abc_set (SingI abc_set)).

An exact proof term for the current goal is HU.

∎