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 (23e07.. x0).
Apply unknownprop_eac7a6683c5ba7aa6ad74545e4a4f065634321e5b116001d3b7a7c41d91b1bf6 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.. x1 x0.
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.
■