Apply H0 with
λ x5 : ι → ι → ο . λ x6 x7 . ∀ x8 : ι → ι → ο . (∀ x9 x10 . x5 x9 x10 ⟶ x8 x9 x10) ⟶ 6fe8d.. x0 x1 x8 x6 x7 leaving 8 subgoals.
Let x5 of type ι → ι → ο be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H1: x0 x6 x7.
Let x8 of type ι → ι → ο be given.
Assume H2: ∀ x9 x10 . x5 x9 x10 ⟶ x8 x9 x10.
Apply unknownprop_b4b184a5ad8ab7cb69711b8ab4d11a3c932ea336f939eb0fb29d7ee6b1126db2 with
x0,
x1,
x8,
x6,
x7.
The subproof is completed by applying H1.
Let x5 of type ι → ι → ο be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H1: x5 x6 x7.
Let x8 of type ι → ι → ο be given.
Assume H2: ∀ x9 x10 . x5 x9 x10 ⟶ x8 x9 x10.
Apply unknownprop_7aca69e6f606c7f0af8e81ab1137c8a1a1c6827be962e013714d23f5b9cc82c8 with
x0,
x1,
x8,
x6,
x7.
Apply H2 with
x6,
x7.
The subproof is completed by applying H1.
Let x5 of type ι → ι → ο be given.
Let x6 of type ι → ι → ο be given.
Assume H1: ∀ x7 x8 . x5 x7 x8 ⟶ x6 x7 x8.
The subproof is completed by applying unknownprop_2c6d593894296c84c8495112a34fbf463ff3a0139d6c76449529901af9854967 with x0, x1, x6.
Let x5 of type ι → ι → ο be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι → ι be given.
Assume H2:
(λ x9 : ι → ι → ο . λ x10 x11 . ∀ x12 : ι → ι → ο . (∀ x13 x14 . x9 x13 x14 ⟶ x12 x13 x14) ⟶ 6fe8d.. x0 x1 x12 x10 x11) x5 x7 32d20...
Assume H3:
∀ x9 . (λ x10 : ι → ι → ο . λ x11 x12 . ∀ x13 : ι → ι → ο . (∀ x14 x15 . x10 x14 x15 ⟶ x13 x14 x15) ⟶ 6fe8d.. x0 x1 x13 x11 x12) (a603a.. x5 x9 x7) (x8 x9) x6.
Let x9 of type ι → ι → ο be given.
Assume H4: ∀ x10 x11 . x5 x10 x11 ⟶ x9 x10 x11.
Apply unknownprop_2e4c9e9bb00a1e00d61dddf5b93521d4a44a5cf34a5d77eca45d066a0b32082a with
x0,
x1,
x9,
x6,
x7,
x8 leaving 3 subgoals.
The subproof is completed by applying H1.
Apply H2 with
x9.
The subproof is completed by applying H4.
Let x10 of type ι be given.
Apply H3 with
x10,
a603a.. x9 x10 x7.
Apply unknownprop_2cf7bc2f5a4dbde4de73cff02382b5f1a3e850236e7d03433e3d2b3d683d34f6 with
x5,
x9,
x10,
x7.
The subproof is completed by applying H4.
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.
Assume H1:
(λ x10 : ι → ι → ο . λ x11 x12 . ∀ x13 : ι → ι → ο . (∀ x14 x15 . x10 x14 x15 ⟶ x13 x14 x15) ⟶ 6fe8d.. x0 x1 x13 x11 x12) x5 x6 (d7cf0.. x8 x9).
Assume H2:
(λ x10 : ι → ι → ο . λ x11 x12 . ∀ x13 : ι → ι → ο . (∀ x14 x15 . x10 x14 x15 ⟶ x13 x14 x15) ⟶ 6fe8d.. x0 x1 x13 x11 x12) x5 x7 x8.
Let x10 of type ι → ι → ο be given.
Assume H3: ∀ x11 x12 . x5 x11 x12 ⟶ x10 x11 x12.
Apply unknownprop_8456f035593e381677ad0ec884ea2dfed6273d70a1e5efa2af3d3eb450e5586f with
x0,
x1,
x10,
x6,
x7,
x8,
x9 leaving 2 subgoals.
Apply H1 with
x10.
The subproof is completed by applying H3.
Apply H2 with
x10.
The subproof is completed by applying H3.
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.
Assume H2:
(λ x10 : ι → ι → ο . λ x11 x12 . ∀ x13 : ι → ι → ο . (∀ x14 x15 . x10 x14 x15 ⟶ x13 x14 x15) ⟶ 6fe8d.. x0 x1 x13 x11 x12) x5 (d7cf0.. x7 x9) x6.
Assume H3:
∀ x10 . (λ x11 : ι → ι → ο . λ x12 x13 . ∀ x14 : ι → ι → ο . ... ⟶ 6fe8d.. x0 x1 x14 x12 x13) ... ... ....