Search for blocks/addresses/...

Proofgold Proof

pf
Apply pair_tuple_fun with λ x0 x1 : ι → ι → ι . ∀ x2 x3 x4 x5 . x0 x2 x3 = x0 x4 x5and (x2 = x4) (x3 = x5).
The subproof is completed by applying pair_inj.