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