Let U be given.
Assume HU: U ∈ top_abc_6.
We will prove U ∈ top_abc_9.
Apply (binunionE' (UPair Empty (UPair a_elt b_elt)) {abc_set} U (U ∈ top_abc_9)) to the current goal.
Assume HU0: U ∈ UPair Empty (UPair a_elt b_elt).
Apply (UPairE U Empty (UPair a_elt b_elt) HU0) 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} ∪ {UPair a_elt b_elt}) {abc_set} Empty (binunionI1 (UPair Empty {a_elt}) {UPair a_elt b_elt} Empty (UPairI1 Empty {a_elt}))).
Assume HUeq: U = UPair a_elt b_elt.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (binunionI1 (UPair Empty {a_elt} ∪ {UPair a_elt b_elt}) {abc_set} (UPair a_elt b_elt) (binunionI2 (UPair Empty {a_elt}) {UPair a_elt b_elt} (UPair a_elt b_elt) (SingI (UPair a_elt b_elt)))).
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.
∎