Search for blocks/addresses/...

Proofgold Proof

pf
Apply pair_tuple_fun with λ x0 x1 : ι → ι → ι . ∀ x2 x3 x4 . x4x0 x2 x3or (∃ x5 . and (x5x2) (x4 = x0 0 x5)) (∃ x5 . and (x5x3) (x4 = x0 1 x5)).
The subproof is completed by applying pairE.