Let p be given.

Assume Hp.

We will prove p 1 ∈ R.

We prove the intermediate claim Hp1: p 1 ∈ (λ_ : set ⇒ R) (p 0).

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

An exact proof term for the current goal is Hp1.

∎