Let U be given.
Assume HU: U ∈ top_abc_1.
We will prove U ∈ top_abc_3.
Apply (UPairE U Empty abc_set HU) to the current goal.
Assume HUeq: U = Empty.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (binunionI1 (UPair Empty {a_elt}) {abc_set} Empty (UPairI1 Empty {a_elt})).
Assume HUeq: U = abc_set.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (binunionI2 (UPair Empty {a_elt}) {abc_set} abc_set (SingI abc_set)).
∎