Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → (ι → ο) → ο be given.
Let x1 of type ι → (ι → ο) → ο be given.
Assume H0: ed32f.. x0 x1.
Let x2 of type ι be given.
Assume H1: ordinal x2.
Assume H2: PNo_lenbdd x2 x0.
Assume H3: PNo_lenbdd x2 x1.
Apply DescrR_i_io_12 with ced99.. x0 x1.
Apply unknownprop_5c4ccf8655ac1c709da38c3d1f61f18da76ac117b3319b22bdde5537970f0904 with x0, x1, x2 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
■