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