Let X, Y and U be given.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ projection_image1 X Y (setprod U Empty).
We will prove x ∈ Empty.
We prove the intermediate claim Hex: ∃y : set, (x,y) ∈ setprod U Empty.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∃y : set, (x0,y) ∈ setprod U Empty) x Hx).
Apply Hex to the current goal.
Let y be given.
Assume Hxy: (x,y) ∈ setprod U Empty.
We prove the intermediate claim HyEmpty: ((x,y) 1) ∈ Empty.
An exact proof term for the current goal is (ap1_Sigma U (λ_ : set ⇒ Empty) (x,y) Hxy).
We prove the intermediate claim HyE: y ∈ Empty.
We will prove y ∈ Empty.
rewrite the current goal using (tuple_2_1_eq x y) (from right to left).
An exact proof term for the current goal is HyEmpty.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE y HyE).
Let x be given.
Assume Hx: x ∈ Empty.
Apply (EmptyE x Hx) to the current goal.
∎