Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. Assume H0: prim1 x1 (f6917.. x0). Apply unknownprop_04b90adbc2ec31bffcbccbbe8e8bda04aa9f95ec157434af0f1f260c2db4f24e with x0, 09364.., x1. The subproof is completed by applying H0. ■