Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: prim1 x2 x0.
Apply unknownprop_0b5b61a66a1ed2eb843dbce5c5f6930c63a284fe5e33704d9f0cc564310ec40b with 94f9e.. x0 (λ x3 . f6917.. x3), 94f9e.. x1 (λ x3 . 09364.. x3), f6917.. x2.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with x0, f6917.., x2.
The subproof is completed by applying H0.