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: 80242.. x1.
Assume H2: prim1 (e4431.. x1) (e4431.. x0).
Assume H3: 099f3.. x1 x0.
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with 56ded.. (e4431.. x0), λ x2 . 099f3.. x2 x0, x1 leaving 2 subgoals.
Apply unknownprop_c00cc223767ee742a69d7b142278ba10f148f15f86cc8e89adc83bb1fda2c95d with x1, x0 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
■