Search for blocks/addresses/...
Proofgold Proof
pf
Apply pair_tuple_fun with
λ x0 x1 :
ι →
ι → ι
.
∀ x2 x3 x4 .
x4
∈
x3
⟶
lam
2
(
λ x5 .
If_i
(
x5
=
0
)
1
x4
)
∈
x1
x2
x3
.
The subproof is completed by applying tupleI1.
■