Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply unknownprop_ea78574cb3264467ecb0cee6dab0f2cbbdf0e0a00f843238d57e1be6acdbe25f with f482f.. 4a7ef.. x0.
Let x1 of type ι be given.
Assume H0: prim1 x1 (f482f.. 4a7ef.. x0).
Claim L1: prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 x1)) 4a7ef..
Apply unknownprop_36581520bffccb98b6c3f6da561f1dee9f6d78d0af9fec9a0855f273170722c3 with 4a7ef.., x0, x1.
The subproof is completed by applying H0.
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x2 . If_i (x2 = 4a7ef..) x0 x1), prim1 x1 4a7ef...
The subproof is completed by applying L1.
■