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