Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 80242.. x0.
Let x1 of type ι be given.
Assume H1: prim1 x1 (5246e.. x0).
Apply unknownprop_9139ee2a8df08ed3f37f7756be409060ff2feed4e0a070067f7d01230efaf1e9 with x0, x1, prim1 x1 (56ded.. (e4431.. x0)) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H2: 80242.. x1.
Assume H3: prim1 (e4431.. x1) (e4431.. x0).
Assume H4: 099f3.. x0 x1.
Apply unknownprop_c00cc223767ee742a69d7b142278ba10f148f15f86cc8e89adc83bb1fda2c95d with x1, x0 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
■