Let z be given.
Assume Hz.
Apply Eps_i_ex (λy ⇒ F y ∧ z = pa (proj0 z) y) to the current goal.
We will prove ∃y, F y ∧ z = pa (proj0 z) y.
Let x and y be given.
Assume Hx Hy.
Assume Hzxy: z = pa x y.
We use y to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hy.
We will prove pa x y = pa (proj0 (pa x y)) y.
Apply CD_proj0_2 x y Hx Hy (λu v ⇒ pa x y = pa v y) to the current goal.
We will prove pa x y = pa x y.
Use reflexivity.