Proofgold Proof

pf
Let x0 of type ι be given. Apply Eps_i_ex with λ x1 . ∀ x2 . iff (prim1 x2 x1) (Subq x2 x0). The subproof is completed by applying unknownprop_681090416aba9c9fb59a588050d70acf83bfc05a81f698de0f540a91644920cc with x0. ■