Search for blocks/addresses/...

Proofgold Proof

pf
Apply pair_tuple_fun with λ x0 x1 : ι → ι → ι . ∀ x2 . ∀ x3 : ι → ι . ∀ x4 . x4x2∀ x5 . x5x3 x4x0 x4 x5lam x2 (λ x6 . x3 x6).
The subproof is completed by applying lamI.