Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: prim1 x0 (4ae4a.. 4a7ef..).
Apply unknownprop_dec2978c0a72cebd51fcab0a380f03d4d80d1ccd8f826d378953148c305a60f0 with 4a7ef.., x0, prim1 x0 (91630.. 4a7ef..) leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H1: prim1 x0 4a7ef...
Apply FalseE with prim1 x0 (91630.. 4a7ef..).
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x0.
The subproof is completed by applying H1.
Assume H1: x0 = 4a7ef...
Apply H1 with λ x1 x2 . prim1 x2 (91630.. 4a7ef..).
The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with 4a7ef...