Proofgold Proof

pf
Let x0 of type (ι → ι) → ο be given. Assume H0: f8922.. x0. Let x1 of type ι be given. Apply unknownprop_410ce78bdfb273d279cabcd4e5cb3d2010a8a0c6262bac3ee000f35bb1402d66 with x0, x1. The subproof is completed by applying H0. ■