Proofgold Proof

pf
Assume H0: ∃ x0 . prim1 x0 4a7ef... Apply H0 with False. Let x0 of type ι be given. Assume H1: prim1 x0 4a7ef... Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x0. The subproof is completed by applying H1. ■