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