Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply xm with empty_p x0, c2f57.. (4326e.. x0) leaving 2 subgoals.
Assume H0: empty_p x0.
Let x1 of type ο be given.
Assume H1: ∀ x2 . (∀ x3 . iff (prim1 x3 x2) (4326e.. x0 x3)) ⟶ x1.
Apply H1 with 91630.. 4a7ef...
Let x2 of type ι be given.
Apply iffI with prim1 x2 (91630.. 4a7ef..), 4326e.. x0 x2 leaving 2 subgoals.
Assume H2: prim1 x2 (91630.. 4a7ef..).
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with 4a7ef.., x2, λ x3 x4 . 4326e.. x0 x4 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_fcc454995021871ff2eb54621f144073c95dc7693368b8b9b68f44dd2b8d3278 with x0.
The subproof is completed by applying H0.
Assume H2: 4326e.. x0 x2.
Claim L3: x2 = 4a7ef..
Apply unknownprop_6b2a29c2c2c396742c3a0e187afc4143e2cfdc098f2744edadb0bb5cb9c4ce61 with x0, x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply L3 with λ x3 x4 . prim1 x4 (91630.. 4a7ef..).
The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with 4a7ef...
Assume H0: not (empty_p x0).
Let x1 of type ο be given.
Assume H1: ∀ x2 . (∀ x3 . iff (prim1 x3 x2) (4326e.. x0 x3)) ⟶ x1.
Apply H1 with x0.
Let x2 of type ι be given.
Apply iffI with prim1 x2 x0, 4326e.. x0 x2 leaving 2 subgoals.
Assume H2: prim1 x2 x0.
Apply unknownprop_547d526f8f61234c156e3c73fa4a8a1aa9a628b58fe16fb380304ebbca858804 with x0, x2.
The subproof is completed by applying H2.
Assume H2: 4326e.. x0 x2.
Apply unknownprop_81e2497d53f26977fa8ca722fab407ecbd3aa74818556ba29653e265699cc106 with x0, x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
■