Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: prim1 x1 x0.
Apply unknownprop_901227726ecb21c0c865a7b1769191cd65e10f479fbeb543b259399303379e3e with x0, x1, 4a7ef.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_e5c1596f5fd6bc2d713145a4e9d44688423a48751f219f9d9d142effb814941e.
Apply unknownprop_d703849eb8e5f2d3b12754a845ec7b0f82607397d42827babfa4298acd2176ee with x0, λ x2 x3 . prim1 x1 x3.
The subproof is completed by applying H0.