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_fb7cd55890d92980315d122000898a4fa27d043f0a778e72117844d8898be28f with x0, x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
■