Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι → ι be given.
Let x4 of type ι → ι be given.
Assume H0:
∀ x5 . In x5 x0 ⟶ In (x3 x5) x2.
Assume H1:
∀ x5 . In x5 x1 ⟶ In (x4 x5) x2.
Let x5 of type ι be given.
Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with
x0,
x1,
x5,
λ x6 . In (combine_funcs x0 x1 x3 x4 x6) x2 leaving 3 subgoals.
The subproof is completed by applying H2.
Let x6 of type ι be given.
Apply unknownprop_d8973abfc5fd9b1197675b2a0610f261f9be335ec7d31dfa5c6a8b518bd2b06a with
x0,
x1,
x3,
x4,
x6,
λ x7 x8 . In x8 x2.
Apply H0 with
x6.
The subproof is completed by applying H3.
Let x6 of type ι be given.
Apply unknownprop_a6e435ff6762616eb80cd4cff726877e67d889d545b7ca4b4b9ea18c1b4ff1e8 with
x0,
x1,
x3,
x4,
x6,
λ x7 x8 . In x8 x2.
Apply H1 with
x6.
The subproof is completed by applying H3.