Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Let x3 of type ι → ι be given.
Assume H1:
∀ x4 . In x4 x0 ⟶ Subq (x2 x4) (x3 x4).
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
lam x0 (λ x4 . x2 x4),
lam x1 (λ x4 . x3 x4).
Let x4 of type ι be given.
Assume H2:
In x4 (lam x0 (λ x5 . x2 x5)).
Apply unknownprop_1eb28f5831a9d21e218b89c238edbbf849d22045bb77ce7cec926a651d1793f0 with
setsum (proj0 x4) (proj1 x4) = x4,
In (proj0 x4) x0,
In (proj1 x4) (x2 (proj0 x4)),
In x4 (lam x1 (λ x5 . x3 x5)) leaving 2 subgoals.
Apply unknownprop_632d5604ed3c6300a4762cec49c7927befabcc480df4aa1142cf8872f14519d7 with
x0,
x2,
x4.
The subproof is completed by applying H2.
Apply H3 with
λ x5 x6 . In x5 (lam x1 (λ x7 . x3 x7)).
Apply unknownprop_1633a25a08ee627a1613041ad1ebe0a4535d0c6ce109cb609e7d9a519dad2f25 with
x1,
x3,
proj0 x4,
proj1 x4 leaving 2 subgoals.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x0,
x1,
proj0 x4 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x2 (proj0 x4),
x3 (proj0 x4),
proj1 x4 leaving 2 subgoals.
Apply H1 with
proj0 x4.
The subproof is completed by applying H4.
The subproof is completed by applying H5.