Let Y be given.
Apply set_ext to the current goal.
Let p be given.
Assume Hp: p ∈ setprod Empty Y.
We will prove p ∈ Empty.
We prove the intermediate claim Hp0: (p 0) ∈ Empty.
An exact proof term for the current goal is (ap0_Sigma Empty (λ_ : set ⇒ Y) p Hp).
An exact proof term for the current goal is (EmptyE (p 0) Hp0 (p ∈ Empty)).
Let p be given.
Assume Hp: p ∈ Empty.
We will prove p ∈ setprod Empty Y.
An exact proof term for the current goal is (EmptyE p Hp (p ∈ setprod Empty Y)).
∎