| 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 19 subgoals.
Apply unknownprop_fc50e0d117923444647ce5345931d8cc81eb09d06240e4778ccb3549485bdf09 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_9c91507c3a6077d4ebecc3dc33a1760547e427611cb29d74e70bed9dbe4a6f88 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_81df60a128fae80ad177096c43febc020e6668c2ec3300f307ac8104ddd57320 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: 0076f.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12. Apply unknownprop_44119d96dba95b881cd883a0b760cd547cd9e183118af3e95a96615d42b45b7e 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_61c3e9437fa94ab44290051267fd51c78818f90b725cbe63487adaf4dd4cd5b0 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_d86e33c54cf795508b6122b17d18fc24340982c7cbe5eaf7decee60502f4700d 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_1d3737dc2d4bf865fad13f7196faf9575ca7013989f1ee56871dd3aa5a4030ef 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_33beedb122311e950a0bb210bb72d5f1f96193122896a174ea7a5f35c15277ff 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_549031ad7a31eb12eb9b5c396ac3c2aaf0d0ae8f6485c8a364f823f6e10dda05 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_11d93635d2187b0f5f1f91b02b9bbbf380bfa1ef3f7a9ef43f124fe3aca5f012 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_9db67721f8cca588b51e8f56313c20c5821ecc271c0c468aad8b95255a7c7cf9 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_8475974612447d7c1aef4369269fab9c581aa71e54b2603c2be6252b88bfd27c 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_d71dbd9ae45e9b954b38b11945898f004265bd2804ae5d325fb6b0b09d0dc350 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_a66adeec3787a44a4d8d95502e4092301d5148bcb91cbb44ba78bbae7a2f6bb3 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_9b5b92854e3350cd2d2ec3f5137cac0f77437b151a2c8d7dfc6160d69bda3ebb 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_3edcd78c7abebed1ac4801f57a00cbb2d169792ce1d74f096bd21408924f2e82 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_dfa3f4cccc785b69005015055eeb7baeee0994938aa0efe0aa7b74dfce661a6e 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_83a9351fff9c84034e8a258ba935b4e7ee2f3c8489e75eb996bfc82d75ceb378 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_29aac9bdac13db05730d2a4a92c5e79bff8178b3c9e8108da27228dff394e96d 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.
■ |
|