Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ u8.
Let x1 of type ι be given.
Assume H1: x1 ∈ u8.
Claim L2: x0 ∈ ordsucc (ordsucc (ordsucc (ordsucc u8)))
Apply ordsuccI1 with ordsucc (ordsucc (ordsucc u8)), x0.
Apply ordsuccI1 with ordsucc (ordsucc u8), x0.
Apply ordsuccI1 with ordsucc u8, x0.
Apply ordsuccI1 with u8, x0.
The subproof is completed by applying H0.
Claim L3: x1 ∈ ordsucc (ordsucc (ordsucc (ordsucc u8)))
Apply ordsuccI1 with ordsucc (ordsucc (ordsucc u8)), x1.
Apply ordsuccI1 with ordsucc (ordsucc u8), x1.
Apply ordsuccI1 with ordsucc u8, x1.
Apply ordsuccI1 with u8, x1.
The subproof is completed by applying H1.
Apply unknownprop_0c825f2c7c09729d7ce0ddc2bcc1c1164def77499abc770e53acff066a542f42 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
■