Search for blocks/addresses/...

Proofgold Proof

pf
Apply ordsucc_inj_contra with u13, u12. The subproof is completed by applying unknownprop_f4e278a6bf4004a90230a7ce4599c33df3b13afc88036ef1d8ff3a4ef834b193. ■