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