Let X, Y and p be given.
We prove the intermediate
claim Hp0X:
p 0 ∈ X.
An
exact proof term for the current goal is
(ap0_Sigma X (λ_ : set ⇒ Y) p Hp).
We prove the intermediate
claim Hp1Y:
p 1 ∈ Y.
An
exact proof term for the current goal is
(ap1_Sigma X (λ_ : set ⇒ Y) p Hp).
We use
(p 0) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hp0X.
We use
(p 1) to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hp1Y.
We prove the intermediate
claim Heta:
p = (p 0,p 1).
An
exact proof term for the current goal is
(setprod_eta X Y p Hp).
rewrite the current goal using Heta (from left to right) at position 1.