Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Assume H0: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2.
Let x2 of type ο be given.
Assume H3:
∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 8b6ad.. x1 x3 x4 x5 x6 ⟶ x2.
Assume H4:
∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 91306.. x1 x3 x4 x5 x6 ⟶ x2.
Assume H5:
∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 65a4c.. x1 x3 x4 x5 x6 ⟶ x2.
Assume H6:
∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 2f869.. x1 x3 x4 x5 x6 ⟶ x2.
Assume H7:
∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ a1d37.. x1 x3 x4 x5 x6 ⟶ x2.
Assume H8:
∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 180f5.. x1 x3 x4 x5 x6 ⟶ x2.
Assume H9:
∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ 9b945.. x1 x3 x4 x5 x6 ⟶ x2.
Apply unknownprop_19c5bea28ef119e30d80f4e7c578df826b34bc3d0b15978a12c7c1b896ec3046 with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x3 of type ι be given.
Assume H12: x3 ∈ x0.
Let x4 of type ι be given.
Assume H13: x4 ∈ x0.
Let x5 of type ι be given.
Assume H14: x5 ∈ x0.
Let x6 of type ι be given.
Assume H15: x6 ∈ x0.
Assume H16: x3 = x4 ⟶ ∀ x7 : ο . x7.
Assume H17: x3 = x5 ⟶ ∀ x7 : ο . x7.
Assume H18: x3 = x6 ⟶ ∀ x7 : ο . x7.
Assume H19: x4 = x5 ⟶ ∀ x7 : ο . x7.
Assume H20: x4 = x6 ⟶ ∀ x7 : ο . x7.
Assume H21: x5 = x6 ⟶ ∀ x7 : ο . x7.
Apply xm with
x1 x3 x4,
x2 leaving 2 subgoals.
Assume H22: x1 x3 x4.
Apply xm with
x1 x3 x5,
x2 leaving 2 subgoals.
Assume H23: x1 x3 x5.
Apply xm with
x1 x3 x6,
x2 leaving 2 subgoals.
Assume H24: x1 x3 x6.
Apply xm with
x1 x4 x5,
x2 leaving 2 subgoals.
Assume H25: x1 x4 x5.
Apply FalseE with
x2.
Apply L10 with
x3,
x4,
x5 leaving 9 subgoals.
The subproof is completed by applying H12.