Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Assume H1:
∀ x2 . In x2 x0 ⟶ In (x1 x2) (Power 1).
Apply unknownprop_9a40b4678ae1931e61346f9ab9e405ec760f2f9d44b3be548b52a8b2ddb78559 with
1,
lam x0 (λ x2 . x1 x2).
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
lam x0 (λ x2 . x1 x2),
1.
Let x2 of type ι be given.
Assume H2:
In x2 (lam x0 (λ x3 . x1 x3)).
Claim L3: x2 = 0
Apply unknownprop_1eb28f5831a9d21e218b89c238edbbf849d22045bb77ce7cec926a651d1793f0 with
setsum (proj0 x2) (proj1 x2) = x2,
In (proj0 x2) x0,
In (proj1 x2) (x1 (proj0 x2)),
x2 = 0 leaving 2 subgoals.
Apply unknownprop_632d5604ed3c6300a4762cec49c7927befabcc480df4aa1142cf8872f14519d7 with
x0,
x1,
x2.
The subproof is completed by applying H2.
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
0,
proj0 x2.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
1,
Sing 0,
proj0 x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_e8598561026ee5bf15479322ab1713bd41b786cd16638ceaff374ea0aee3dd94.
Apply unknownprop_80adb48ef5eb67bcd09adc7406871ab43353cad2bcfe3193f4b879331fdfb0b9 with
1,
x0,
proj0 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
0,
proj1 x2.
Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
1,
Sing 0,
proj1 x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_e8598561026ee5bf15479322ab1713bd41b786cd16638ceaff374ea0aee3dd94.
Apply unknownprop_80adb48ef5eb67bcd09adc7406871ab43353cad2bcfe3193f4b879331fdfb0b9 with
1,
x1 (proj0 x2),
proj1 x2 leaving 2 subgoals.
Apply H1 with
proj0 x2.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply H3 with
λ x3 x4 . x3 = 0.
Apply L6 with
λ x3 x4 . setsum x4 (proj1 x2) = 0.
Apply L7 with
λ x3 x4 . setsum 0 x4 = 0.
The subproof is completed by applying unknownprop_92e9d75f0c2736874e0d273c2aebd9f3628211a178962928cb4fc08e22c09f27.
Apply L3 with
λ x3 x4 . In x4 1.
The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.