Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply proj0_ap_0 with x0, λ x1 x2 . setsum x1 (ap x0 1)x0.
Apply proj1_ap_1 with x0, λ x1 x2 . setsum (proj0 x0) x1x0.
The subproof is completed by applying pair_eta_Subq_proj with x0.