Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: ordinal x0.
Assume H1: prim1 (15418.. x1 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x0.
Apply unknownprop_a8878c29309829d150241e26a9b77d4615ecfcc3ff20770f3d99077abbcc4b0d with x1.
Apply ordinal_Hered with x0, (λ x2 . 15418.. x2 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
■