Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: empty_p x0.
Let x1 of type ι be given.
Assume H1: 4326e.. x0 x1.
Apply H1 with x1 = 4a7ef.. leaving 2 subgoals.
Assume H2: prim1 x1 x0.
Apply FalseE with x1 = 4a7ef...
Apply H0 with x1.
The subproof is completed by applying H2.
Assume H2: and (empty_p x0) (empty_p x1).
Apply H2 with x1 = 4a7ef...
Assume H3: empty_p x0.
Assume H4: empty_p x1.
Apply unknownprop_d965d0c416b693fce9f9d45ca5dffd69bdac5d2ed66b83b98a0bc21514722eda with x1.
The subproof is completed by applying H4.
■