Let x be given.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ {x}.
We prove the intermediate claim Hyeq: y = x.
An exact proof term for the current goal is (SingE x y Hy).
rewrite the current goal using Hyeq (from left to right).
An exact proof term for the current goal is (UPairI1 x x).
Let y be given.
Assume Hy: y ∈ {x,x}.
We prove the intermediate claim Hyeq: y = x.
Apply (UPairE y x x Hy (y = x)) to the current goal.
Assume H1.
An exact proof term for the current goal is H1.
Assume H1.
An exact proof term for the current goal is H1.
rewrite the current goal using Hyeq (from left to right).
An exact proof term for the current goal is (SingI x).
∎