Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
ap (lam x0 (λ x3 . x1 x3)) x2,
x1 x2 leaving 2 subgoals.
Let x3 of type ι be given.
Assume H1:
In x3 (ap (lam x0 (λ x4 . x1 x4)) x2).
Apply unknownprop_762358d061bd2484ba81471a0b72cf827e125ecce5f1471d9abb4ee5039695f2 with
lam x0 (λ x4 . x1 x4),
x2,
x3.
The subproof is completed by applying H1.
Apply unknownprop_1675af88344c4eff7077f223dc9d7368946dad1693a26309b0fe16976c1762ed with
x0,
x1,
x2,
x3.
The subproof is completed by applying L2.
Let x3 of type ι be given.
Assume H1:
In x3 (x1 x2).
Apply unknownprop_5790343a8368d4f3aa514e68a19a3e4824006be2aed8a0a7a707f542e4c79154 with
lam x0 (λ x4 . x1 x4),
x2,
x3.
Apply unknownprop_1633a25a08ee627a1613041ad1ebe0a4535d0c6ce109cb609e7d9a519dad2f25 with
x0,
λ x4 . x1 x4,
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.