Search for blocks/addresses/...

Proofgold Proof

pf
Apply pair_tuple_fun with λ x0 x1 : ι → ι → ι . ∀ x2 x3 x4 . x0 x3 x4x2x4ap x2 x3.
The subproof is completed by applying apI.