Proofgold Proof

pf
Let x0 of type ι → ι → ι be given. Assume H0: prim1 (λ x1 . prim1 (x0 x1)) = 236c6... Apply unknownprop_72aa27d3b3e4d7983fc8b7d5f502eb77af6606394c5a828f035e5bab238fe78c with x0. Let x1 of type ι → ι → ο be given. The subproof is completed by applying H0 with λ x2 x3 . x1 x3 x2. ■