Search for blocks/addresses/...

Proofgold Proof

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