Search for blocks/addresses/...

Proofgold Proof

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