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.
Apply unknownprop_770b8f17a039779f81c6ba159d7c41f050bf8e34aeb13f5bde62972172ae2585 with
x0,
x1,
x2,
x3,
x4,
x5,
x6,
∃ x7 . and (prim1 x7 x0) (∃ x8 . and (prim1 x8 (x1 x7)) (∃ x9 . and (prim1 x9 (x2 x7 x8)) (∃ x10 . and (prim1 x10 (x3 x7 x8 x9)) (and (x4 x7 x8 x9 x10) (x6 = x5 x7 x8 x9 x10))))) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x7 of type ι be given.
Let x8 of type ι be given.
Assume H2:
prim1 x8 (x1 x7).
Let x9 of type ι be given.
Assume H3:
prim1 x9 (x2 x7 x8).
Let x10 of type ι be given.
Assume H4:
prim1 x10 (x3 x7 x8 x9).
Assume H5: x4 x7 x8 x9 x10.
Assume H6: x6 = x5 x7 x8 x9 x10.
Let x11 of type ο be given.
Assume H7:
∀ x12 . and (prim1 x12 x0) (∃ x13 . and (prim1 x13 (x1 x12)) (∃ x14 . and (prim1 x14 (x2 x12 x13)) (∃ x15 . and (prim1 x15 (x3 x12 x13 x14)) (and (x4 x12 x13 x14 x15) (x6 = x5 x12 x13 x14 x15))))) ⟶ x11.
Apply H7 with
x7.
Apply andI with
prim1 x7 x0,
∃ x12 . and (prim1 x12 (x1 x7)) (∃ x13 . and (prim1 x13 (x2 x7 x12)) (∃ x14 . and (prim1 x14 (x3 x7 x12 x13)) (and (x4 x7 x12 x13 x14) (x6 = x5 x7 x12 x13 x14)))) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x12 of type ο be given.
Assume H8:
∀ x13 . and (prim1 x13 (x1 x7)) (∃ x14 . and (prim1 x14 (x2 x7 x13)) (∃ x15 . and (prim1 x15 (x3 x7 x13 x14)) (and (x4 x7 x13 x14 x15) (x6 = x5 x7 x13 x14 x15)))) ⟶ x12.
Apply H8 with
x8.
Apply andI with
prim1 x8 (x1 x7),
∃ x13 . and (prim1 x13 (x2 x7 x8)) (∃ x14 . and (prim1 x14 (x3 x7 x8 x13)) (and (x4 x7 x8 x13 x14) (x6 = x5 x7 x8 x13 x14))) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x13 of type ο be given.
Assume H9:
∀ x14 . and (prim1 x14 (x2 x7 x8)) (∃ x15 . and (prim1 x15 (x3 x7 ... ...)) ...) ⟶ x13.