Let p be given.

Assume Hp.

We will prove p 0 ∈ R.

An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) p Hp).

∎