Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: 4ae4a.. x0 = 4a7ef... Apply unknownprop_e673ffa43d637e4ad1597cb67f33a29ca918f2b4d1035a90a508f3118c8fa9a3 with x0. Let x1 of type ι → ι → ο be given. The subproof is completed by applying H0 with λ x2 x3 . x1 x3 x2. ■