Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι → ι be given.
Let x3 of type ι → ι → ι → ι be given.
Let x4 of type ι → ι → ι → ι → ο be given.
Let x5 of type ι → ι → ι → ι → ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H1:
prim1 x7 (x1 x6).
Let x8 of type ι be given.
Assume H2:
prim1 x8 (x2 x6 x7).
Let x9 of type ι be given.
Assume H3:
prim1 x9 (x3 x6 x7 x8).
Assume H4: x4 x6 x7 x8 x9.
Apply UnionI with
94f9e.. x0 (λ x10 . 85402.. (x1 x10) (x2 x10) (x3 x10) (x4 x10) (x5 x10)),
x5 x6 x7 x8 x9,
85402.. (x1 x6) (x2 x6) (x3 x6) (x4 x6) (x5 x6) leaving 2 subgoals.
Apply unknownprop_b4e2643453112fa388cba1af91cd086309e1961c3fc861629c6ede7103e4d443 with
x1 x6,
x2 x6,
x3 x6,
x4 x6,
x5 x6,
x7,
x8,
x9 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply unknownprop_4785a7374559bd7d78314ce01f76cab97234c9b29cfa5b01c939c64f8ccf18e4 with
x0,
λ x10 . 85402.. (x1 x10) (x2 x10) (x3 x10) (x4 x10) (x5 x10),
x6.
The subproof is completed by applying H0.