Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Assume H0:
In x2 (Pi x0 (λ x3 . x1 x3)).
Let x3 of type ι be given.
Assume H1:
In x3 (Pi x0 (λ x4 . x1 x4)).
Assume H2:
∀ x4 . In x4 x0 ⟶ Subq (ap x2 x4) (ap x3 x4).
Apply unknownprop_c20579f7ec03c9b411c1afcdcbd6eb7f887b4dea35b13dd2fe5a71172b6554fe with
x0,
x1,
x2,
Subq x2 x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H4:
∀ x4 . In x4 x0 ⟶ In (ap x2 x4) (x1 x4).
Apply unknownprop_c20579f7ec03c9b411c1afcdcbd6eb7f887b4dea35b13dd2fe5a71172b6554fe with
x0,
x1,
x3,
Subq x2 x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H6:
∀ x4 . In x4 x0 ⟶ In (ap x3 x4) (x1 x4).
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
x2,
x3.
Let x4 of type ι be given.
Apply andE with
setsum_p x4,
In (ap x4 0) x0,
In x4 x3 leaving 2 subgoals.
Apply H3 with
x4.
The subproof is completed by applying H7.
Apply unknownprop_56bd0714abefd533b13603d171a24196c02fb0b6a0af8036287a8ec089f8957d with
λ x5 x6 : ι → ο . x6 x4 ⟶ In (ap x4 0) x0 ⟶ In x4 x3.
Assume H9:
In (ap x4 0) x0.
Apply H8 with
λ x5 x6 . In x5 x3.
Apply unknownprop_762358d061bd2484ba81471a0b72cf827e125ecce5f1471d9abb4ee5039695f2 with
x3,
ap x4 0,
ap x4 1.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
ap x2 (ap x4 0),
ap x3 (ap x4 0),
ap x4 1 leaving 2 subgoals.
Apply H2 with
ap x4 0.
The subproof is completed by applying H9.
Apply unknownprop_5790343a8368d4f3aa514e68a19a3e4824006be2aed8a0a7a707f542e4c79154 with
x2,
ap x4 0,
ap x4 1.
Apply H8 with
λ x5 x6 . In x6 x2.
The subproof is completed by applying H7.