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: x2 ∈ x0.
Let x3 of type ι be given.
Apply H5 with
∀ x4 : ο . x4 leaving 5 subgoals.
Let x4 of type ι be given.
Assume H6: x4 ∈ x3.
Let x5 of type ι be given.
Assume H7: x5 ∈ x3.
Let x6 of type ι be given.
Assume H8: x6 ∈ x3.
Let x7 of type ι be given.
Assume H9: x7 ∈ x3.
Let x8 of type ι be given.
Assume H10: x8 ∈ x3.
Let x9 of type ι be given.
Assume H11: x9 ∈ x3.
Let x10 of type ι be given.
Assume H12: x10 ∈ x3.
Let x11 of type ι be given.
Assume H13: x11 ∈ x3.
Let x12 of type ι be given.
Assume H14: x12 ∈ x3.
Assume H15:
889b5.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12.
Apply unknownprop_1a198e8c0b4779e4ddab69f3eecdcd4ded31cd8e9d0a43a476ba59653895cbe7 with
x3,
x0,
x1,
x2,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11,
x12 leaving 15 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H15.
Let x4 of type ι be given.
Assume H6: x4 ∈ x3.
Let x5 of type ι be given.
Assume H7: x5 ∈ x3.
Let x6 of type ι be given.
Assume H8: x6 ∈ x3.
Let x7 of type ι be given.
Assume H9: x7 ∈ x3.
Let x8 of type ι be given.
Assume H10: x8 ∈ x3.
Let x9 of type ι be given.
Assume H11: x9 ∈ x3.
Let x10 of type ι be given.
Assume H12: x10 ∈ x3.
Let x11 of type ι be given.
Assume H13: x11 ∈ x3.
Let x12 of type ι be given.
Assume H14: x12 ∈ x3.
Assume H15:
71ae3.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12.
Apply unknownprop_ac2150a773971ec114d0379e0982b508b39b59f4ee5d9d82d62b68cf83ce5399 with
x3,
x0,
x1,
x2,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11,
x12 leaving 15 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H15.
Let x4 of type ι be given.
Assume H6: x4 ∈ x3.
Let x5 of type ι be given.
Assume H7: x5 ∈ x3.
Let x6 of type ι be given.
Assume H8: x6 ∈ x3.
Let x7 of type ι be given.
Assume H9: x7 ∈ x3.
Let x8 of type ι be given.
Assume H10: x8 ∈ x3.
Let x9 of type ι be given.
Assume H11: x9 ∈ x3.
Let x10 of type ι be given.
Assume H12: x10 ∈ x3.
Let x11 of type ι be given.
Assume H13: x11 ∈ x3.
Let x12 of type ι be given.
Assume H14: x12 ∈ x3.
Assume H15:
df026.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12.
Apply unknownprop_0c8a0b05ede769d37382736c88badefd606f60254da20f5025e6212ac39837e5 with
x3,
x0,
x1,
x2,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11,
x12 leaving 15 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H15.
Let x4 of type ι be given.
Assume H6: x4 ∈ x3.
Let x5 of type ι be given.
Assume H7: x5 ∈ x3.
Let x6 of type ι be given.
Assume H8: x6 ∈ x3.
Let x7 of type ι be given.
Assume H9: ... ∈ ....