| 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 18 subgoals.
Apply unknownprop_33ec366723a94310cccf1c559c9b05e13de04ab2ee9610f8b369d31d479f6d91 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_e7f095a225142976bfaee3d83b2db123636e5c650082a713a548c2d832cef0da 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_94a9eabe0cc8081e157248f41d2728184e3d92492878871e48b199f2eea6ced6 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_d6cf8a1ba7f998317b509950cca2721a99ff24b213888ecf4a1ca80bee4a855d 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_395a5eb91f7708c102cbff3248e3d1602072590d485eb7917f8f1ad1187333ba 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_b7d0544003d080990c32d1dbcdf9e8a1bcebd4d41fc6671e7793216f6f72b4f7 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_27b7fb3c033e168e42299ee5bfb863fbcb57af2bcda8c8f69304c92e6d63e175 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_c9aac90d1a395d45b2cc862ba6d1ef5d1f688771d6c0e4c076ff25feb10735e8 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_7c3c3abb45f3303cababf09bcc3979f7b397fe22e2a4f7c27e5bb79624278a78 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_b3c2c91b825da43e476b8258e017e9e3ce739b9fdc3558cf9f630b9f25a51911 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_af5450618dfacdf634f12a5016547b92f451a6cc3406a472253675226a04014e 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_149f8504f3d4134e300ec00ee749f5a79c57c4da419e4b23e08aa1ea6be17d38 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: 23926.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12. Apply unknownprop_8e252e5ed769a2f0a5ec8c0d840b0e083554b8af1998963e8cd9d88f1fb5efc3 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_380f88c4b921f110a5f6622f3baa54e4a9458c42d481c3d6e3e528a35d60a794 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_87aa183774f3040cd2e57dd8ebb412d7bafe0e55e72e4e684ae8eb007ebac4dc 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_ba061a12d609c986594e5b68f93811fed0e82b1a3dd76fe3c887de1f195f1306 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_92d42fbd3a8a15274b9e3e2fbccc3f17f3c63526c7c99581cae9d0cb02c22d36 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_c4de47c050e0618dff8ec99a4f13d5f6b6617e8701569ee89d1ce5aa1af13e15 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.
■ |
|