Search for blocks/addresses/...
Proofgold Proof
pf
Apply add_SNo_add_CSNo with
1
,
1
,
λ x0 x1 .
x0
=
2
leaving 3 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_1.
The subproof is completed by applying add_SNo_1_1_2.
■