Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
Sing
2
∈
Sing
(
Sing
1
)
.
Claim L1:
1
∈
Sing
2
Apply SingE with
Sing
1
,
Sing
2
,
λ x0 x1 .
1
∈
x1
leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SingI with
1
.
Apply neq_1_2.
Apply SingE with
2
,
1
.
The subproof is completed by applying L1.
■