Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply set_ext with aae7a.. 4a7ef.. x0, f6917.. x0 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H0: prim1 x1 (aae7a.. 4a7ef.. x0).
Apply unknownprop_c7550417d862f27710857dc7f3a47fd61afe15d66581922367eb5c5641bfab12 with 4a7ef.., x0, x1, prim1 x1 (f6917.. x0) leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1: ∃ x2 . and (prim1 x2 4a7ef..) (x1 = f6917.. x2).
Apply exandE_i with λ x2 . prim1 x2 4a7ef.., λ x2 . x1 = f6917.. x2, prim1 x1 (f6917.. x0) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: prim1 x2 4a7ef...
Apply FalseE with x1 = f6917.. x2prim1 x1 (f6917.. x0).
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x2.
The subproof is completed by applying H2.
Assume H1: ∃ x2 . and (prim1 x2 x0) (x1 = 09364.. x2).
Apply exandE_i with λ x2 . prim1 x2 x0, λ x2 . x1 = 09364.. x2, prim1 x1 (f6917.. x0) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: prim1 x2 x0.
Assume H3: x1 = 09364.. x2.
Apply H3 with λ x3 x4 . prim1 x4 (f6917.. x0).
Apply unknownprop_cb49923233a17bfcdaaace11cf639914b23f1e115c13971fdab382102fec388a with x0, x2.
The subproof is completed by applying H2.
Let x1 of type ι be given.
Assume H0: prim1 x1 (f6917.. x0).
Apply exandE_i with λ x2 . prim1 x2 x0, λ x2 . x1 = 09364.. x2, prim1 x1 (aae7a.. 4a7ef.. x0) leaving 2 subgoals.
Apply unknownprop_a63bdc277f1325cdd852a9c9272f39668f29a68974de510ddb75e64c4c429794 with x0, x1.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H1: prim1 x2 x0.
Assume H2: x1 = 09364.. x2.
Apply H2 with λ x3 x4 . prim1 x4 (aae7a.. 4a7ef.. x0).
Apply unknownprop_21bfd05a2dded69408d4a77ad07f3965317c49d7fa73834904d6def11389f597 with 4a7ef.., x0, x2.
The subproof is completed by applying H1.