Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_390fca52cd547a01287e1b72ed6b3adcf1f85df24d75a2f5e1a912006e833a34 with
λ x3 x4 : ι → ι → ι . In x2 (x4 x0 x1).
Apply unknownprop_d4bb68cbfba730ad1b1ee2c6901fadf3c573cb615fac3296f9bb52128e37668a with
x1,
x2,
λ x3 x4 . In x3 (ReplSep x0 (λ x5 . ∃ x6 . x5 = setsum x1 x6) (λ x5 . proj1 x5)).
Apply unknownprop_8d2d2cad5b49b3f5b663b34a4b05b87bd91c0d0340dcf2eab94b6803f88f2fd8 with
x0,
λ x3 . ∃ x4 . x3 = setsum x1 x4,
proj1,
setsum x1 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ο be given.
Apply H1 with
x2.
Let x4 of type ι → ι → ο be given.
The subproof is completed by applying H2.