Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: 21.
Apply ordsuccE with 0, 2, False leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying EmptyE with 2.
The subproof is completed by applying neq_2_0.