Let x0 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
setexp x0 0,
1 leaving 2 subgoals.
Let x1 of type ι be given.
Claim L1:
In x1 (Pi 0 (λ x2 . x0))Apply unknownprop_7e65b2cb934666fa04709e34a9ec7a8cd447de0a66d9962491fb608c410f4e23 with
0,
x0,
x1.
The subproof is completed by applying H0.
Apply unknownprop_c20579f7ec03c9b411c1afcdcbd6eb7f887b4dea35b13dd2fe5a71172b6554fe with
0,
λ x2 . x0,
x1,
In x1 1 leaving 2 subgoals.
The subproof is completed by applying L1.
Assume H3:
∀ x2 . In x2 0 ⟶ In (ap x1 x2) x0.
Claim L4: x1 = 0
Apply unknownprop_fe7ff313be3d0b9f2334c12982636aff94f7603137e8053506a95c79965309c2 with
x1.
Let x2 of type ι be given.
Apply unknownprop_b30a94f49240f0717f4ecb200a605aa8a4e6dad6dc5d1afa60c37866ee96baab with
x2,
x1.
Apply andE with
setsum_p x2,
In (ap x2 0) 0,
False leaving 2 subgoals.
Apply H2 with
x2.
The subproof is completed by applying H4.
The subproof is completed by applying unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
ap x2 0.
Apply L4 with
λ x2 x3 . In x3 1.
The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.
Let x1 of type ι be given.
Apply unknownprop_7f6501f9f8c19f5c2cddf4168679e2ff20a237333cd0d098eed3a3984bc044c0 with
x1,
λ x2 . In x2 (setexp x0 0) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_9579ad195736876dd5df05c987aa079a6bacb25bc99006ef7b42c5a972f244df with
0,
x0,
0.
Apply unknownprop_1a1eed9c2e0652a509eabe7b8f07e31768cab0357ad1d97cb464202e3d371a17 with
0,
λ x2 . x0,
0 leaving 2 subgoals.
Let x2 of type ι be given.
Apply FalseE with
and (setsum_p x2) (In (ap x2 0) 0).
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x2.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Apply FalseE with
In (ap 0 x2) ((λ x3 . x0) x2).
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x2.
The subproof is completed by applying H1.