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
5bab1.. x0 x1 leaving 5 subgoals.
Apply unknownprop_537f5f6b770fb7dddebb81daf4ea4e11c94c68a4756a2c7d86f7603bb8cbe98c with
x0,
x1,
x2,
x3 leaving 5 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.
Apply unknownprop_aa6f7838aa9d38fb8dde3d2900e7ea384f4056db108acb3b0b51403d0459ade7 with
x0,
x1,
x2,
x3 leaving 5 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.
Apply unknownprop_1edc3e328fa0d545d11290c795ec655fd4210c06be0532bb45b3aeaf2f1d76e4 with
x0,
x1,
x2,
x3 leaving 5 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.
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:
1b69c.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12.
Apply unknownprop_7d0073d50c2fa98d304ef1fa3e39630206d0515f4f85deded3ca8986edcd3932 with
x3,
x0,
x1,
x2,
x4,
x5,
x6,
x7,
x8,
x9,
x10,
x11,
x12,
5bab1.. x0 x1 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.
Apply unknownprop_7a38cb7f8fbdb93cabf6212d4b5edeefa44c135faa782b10003cd791f67ed0f0 with
x0,
x1,
x2,
x3 leaving 5 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.