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