Proofgold Proof

pf

Let x0 of type ι be given.

Let x1 of type ι → ο be given.

Apply unknownprop_ee0b4b64aba8e6af97035d72b359ab8e1ae1e5e06024c58477c9410cad648356 with λ x2 x3 : ι → (ι → ο) → (ι → ο) → ο . x3 x0 x1 x1.

Let x2 of type ι be given.

Assume H0: In x2 x0.

The subproof is completed by applying unknownprop_00f3675b03ca269a8c79b213adec0a88ac62c517087fb97bcaaa311794c5691c with x1 x2.

■