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.
Let x8 of type ι be given.
Let x9 of type ο be given.
Assume H1:
∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 (x1 x10) ⟶ ∀ x12 . prim1 x12 (x2 x10 x11) ⟶ ∀ x13 . prim1 x13 (x3 x10 x11 x12) ⟶ ∀ x14 . prim1 x14 (x4 x10 x11 x12 x13) ⟶ ∀ x15 . prim1 x15 (x5 x10 x11 x12 x13 x14) ⟶ x6 x10 x11 x12 x13 x14 x15 ⟶ x8 = x7 x10 x11 x12 x13 x14 x15 ⟶ x9.
Apply UnionE_impred with
94f9e.. x0 (λ x10 . 2aab0.. (x1 x10) (x2 x10) (x3 x10) (x4 x10) (x5 x10) (x6 x10) (x7 x10)),
x8,
x9 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x10 of type ι be given.
Assume H3:
prim1 x10 (94f9e.. x0 (λ x11 . 2aab0.. (x1 x11) (x2 x11) (x3 x11) (x4 x11) (x5 x11) (x6 x11) (x7 x11))).
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with
x0,
λ x11 . 2aab0.. (x1 x11) (x2 x11) (x3 x11) (x4 x11) (x5 x11) (x6 x11) (x7 x11),
x10,
x9 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x11 of type ι be given.
Assume H5:
x10 = 2aab0.. (x1 x11) (x2 x11) (x3 x11) (x4 x11) (x5 x11) (x6 x11) (x7 x11).
Claim L6:
prim1 x8 (2aab0.. (x1 x11) (x2 x11) (x3 x11) (x4 x11) (x5 x11) (x6 x11) (x7 x11))Apply unknownprop_d894af75fae006d7c8f01f155e4cae4c3cffbd328d070aad2fe18b3235b74596 with
x1 x11,
x2 x11,
x3 x11,
x4 x11,
x5 x11,
x6 x11,
x7 x11,
x8,
x9 leaving 2 subgoals.
The subproof is completed by applying L6.
Let x12 of type ι be given.
Assume H7:
prim1 x12 (x1 x11).
Let x13 of type ι be given.
Assume H8:
prim1 x13 (x2 x11 x12).
Let x14 of type ι be given.
Assume H9:
prim1 x14 (x3 x11 x12 x13).
Let x15 of type ι be given.
Assume H10:
prim1 x15 (x4 x11 x12 x13 x14).
Let x16 of type ι be given.
Assume H11:
prim1 x16 (x5 x11 x12 x13 x14 x15).
Assume H12: x6 x11 x12 x13 x14 x15 x16.
Assume H13: x8 = x7 x11 x12 x13 x14 x15 x16.
Apply H1 with
x11,
x12,
x13,
x14,
x15,
x16 leaving 8 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
The subproof is completed by applying H13.