Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply xm with ∃ x1 . prim1 x1 x0, or (x0 = 4a7ef..) (∃ x1 . prim1 x1 x0) leaving 2 subgoals.
Assume H0: ∃ x1 . prim1 x1 x0.
Apply orIR with x0 = 4a7ef.., ∃ x1 . prim1 x1 x0.
The subproof is completed by applying H0.
Assume H0: not (∃ x1 . prim1 x1 x0).
Apply orIL with x0 = 4a7ef.., ∃ x1 . prim1 x1 x0.
Apply set_ext with x0, 4a7ef.. leaving 2 subgoals.
Let x1 of type ι be given.
Assume H1: prim1 x1 x0.
Apply FalseE with prim1 x1 4a7ef...
Apply H0.
Let x2 of type ο be given.
Assume H2: ∀ x3 . prim1 x3 x0x2.
Apply H2 with x1.
The subproof is completed by applying H1.
The subproof is completed by applying unknownprop_eb7b9ba678ea2ffa85e842fbfec0cd6c41d790582268f13f83a490db67168c54 with x0.