Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_3c224b4e9e4b1cc27f6e09753a4c2a921c2c76dd1bd8aa1b280d8e146202f8fd with
λ x2 x3 : ι → ι . In x1 (x3 x0) ⟶ In (setsum 1 x1) x0.
Apply unknownprop_e88b17fc7534a834a3292f38867e04234c9b0d119c42f884c32fbabae05b0d7e with
λ x2 x3 : ι → ι . In (x2 x1) x0.
Apply unknownprop_021a576837934491f6aaf936d4c5a9c68d45f2b77fcd13cc395cfdeec72f7dac with
x0,
λ x2 . ∃ x3 . Inj1 x3 = x2,
Unj,
x1,
In (Inj1 x1) x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Assume H2:
∃ x3 . Inj1 x3 = x2.
Apply H2 with
In (Inj1 x1) x0.
Let x3 of type ι be given.
Apply H3 with
λ x4 x5 . In (Inj1 x5) x0.
Apply H4 with
λ x4 x5 . In (Inj1 (Unj x4)) x0.
Apply unknownprop_56702b69fe31029117149136473717807c61136823145112690cf6c5e3fd3b5f with
x3,
λ x4 x5 . In (Inj1 x5) x0.
Apply H4 with
λ x4 x5 . In x5 x0.
The subproof is completed by applying H1.