Search for blocks/addresses/...

Proofgold Proof

pf
Apply pair_tuple_fun with λ x0 x1 : ι → ι → ι . ∀ x2 . ∀ x3 : ι → ι . ∀ x4 . x4lam x2 (λ x5 . x3 x5)∃ x5 . and (x5x2) (∃ x6 . and (x6x3 x5) (x4 = x0 x5 x6)).
The subproof is completed by applying lamE.