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