Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι → ι be given. Let x2 of type ι be given. Apply proj0_ap_0 with x2, λ x3 x4 . x2 ∈ lam x0 (λ x5 . x1 x5) ⟶ x3 ∈ x0. The subproof is completed by applying proj0_Sigma with x0, λ x3 . x1 x3, x2. ■