| pf |
|---|
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 9 subgoals.
Apply unknownprop_98829eba4b48424dc5b59df92e190569509072d71245a9d772a4817028ca36c9 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_abb8482eeeb1ae66e0ac8fd7ca7194d4c28509f0768e81fe2fe205c529489480 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_e7f1948087d3570d8d96910a26af23d53df451c2b2ecac9d5b1d02e888501602 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: ed1c7.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12. Apply unknownprop_a9af3ec656c05dd4a2019ddd75caafa2e05f9d537eacdbb0bbe2740e0117f1b9 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_1d3fd099d3d351a2f20f2c9d8c29d9b161c2ad9e3ba3251b3381b61ed0c20cb9 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_2c631b6774da22e6a2dd38daa367764111f9de934037accee6f9c187054fab2f 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_9d6f526cc88f0bd5edd1fcae998a118befaec60c22af3ca9823afca31fc0ee92 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_ef672afa01f044e628019275e88ea24972c5817b2f8a8db108bbed33a31551de 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_1ed70ea28ac0088d3771a276efa9ef449fb30b1060053581ea2aa4d153243cbc 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.
■ |
|