Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply set_ext with 22ca9.. (aae7a.. x0 x1), x1 leaving 2 subgoals.
Let x2 of type ι be given.
Assume H0: prim1 x2 (22ca9.. (aae7a.. x0 x1)).
Apply unknownprop_b99ca2c7d71b08f49bc694a4f2f3716eab3cfc0a3351cd23d1373c39bcb2b95c with x0, x1, x2.
Apply unknownprop_faa0906fd70676f18d9a02c8ff6587696be109a33d66d00ec0a508d4784f9592 with aae7a.. x0 x1, x2.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H0: prim1 x2 x1.
Apply unknownprop_0b996f3ce0151f58af219429b661039e0f6628ef50f5457c6338b0fd3feaa164 with aae7a.. x0 x1, x2.
Apply unknownprop_b4a3840982f4171d50a8011f1d1ddb72ad2a6c5880e9b141f24bf23602367bb7 with x0, x1, x2.
The subproof is completed by applying H0.