| pf |
|---|
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply set_ext with 0ac37.. x0 (d3786.. x1 x2), d3786.. (0ac37.. x0 x1) (0ac37.. x0 x2) leaving 2 subgoals.
Apply unknownprop_ca91282e0ce9e0658e00929623a7308f21757843a59143f77f3c318bcf850a5e with 0ac37.. x0 x1, 0ac37.. x0 x2, 0ac37.. x0 (d3786.. x1 x2) leaving 2 subgoals.
Apply unknownprop_c16c0737d29e3b3e820cf0e7f73a8868a90e8434c78c164566097cca1a566416 with x0, d3786.. x1 x2, 0ac37.. x0 x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_888c4c61f9af73a08c8a3d54aaeed5dafb313e52bc146db81320dd33dcdade2c with x0, x1.
Apply Subq_tra with d3786.. x1 x2, x1, 0ac37.. x0 x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_8f5bf12cfaed0ffd6b0b2703f40521e4f47dbe14ca71e17ebdcebdd96c630d67 with x1, x2.
The subproof is completed by applying unknownprop_0fa3c716de2f83f3d57854877ac4d59bd5007991ec359a1e0159fb506bca2548 with x0, x1.
Apply unknownprop_c16c0737d29e3b3e820cf0e7f73a8868a90e8434c78c164566097cca1a566416 with x0, d3786.. x1 x2, 0ac37.. x0 x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_888c4c61f9af73a08c8a3d54aaeed5dafb313e52bc146db81320dd33dcdade2c with x0, x2.
Apply Subq_tra with d3786.. x1 x2, x2, 0ac37.. x0 x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_8c33f2993dbd85b3390e51467f1f34c3a7271a7424f5fa69403f3fe6fa095bed with x1, x2.
The subproof is completed by applying unknownprop_0fa3c716de2f83f3d57854877ac4d59bd5007991ec359a1e0159fb506bca2548 with x0, x2.
Let x3 of type ι be given.
Apply unknownprop_1ac99d32a7ae5dc08fd640ea6c8b661df6b3535fe85e88b30b17c3701cb4c7ce with 0ac37.. x0 x1, 0ac37.. x0 x2, x3, prim1 x3 (0ac37.. x0 (d3786.. x1 x2)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_b46721c187c37140cbae22d356b00ba89f4126d81d8665e4be15b5a58c78d06f with x0, x1, x3, prim1 x3 (0ac37.. x0 (d3786.. x1 x2)) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying unknownprop_0b5b61a66a1ed2eb843dbce5c5f6930c63a284fe5e33704d9f0cc564310ec40b with x0, d3786.. x1 x2, x3.
Apply unknownprop_b46721c187c37140cbae22d356b00ba89f4126d81d8665e4be15b5a58c78d06f with x0, x2, x3, prim1 x3 (0ac37.. x0 (d3786.. x1 x2)) leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_0b5b61a66a1ed2eb843dbce5c5f6930c63a284fe5e33704d9f0cc564310ec40b with x0, d3786.. x1 x2, x3.
Apply unknownprop_e4d6e0bfb4ef6d52ee13edd54a77c8cc7f0a3af8ffb1b8da66d4f98842dd28b5 with x0, d3786.. x1 x2, x3.
Apply unknownprop_0eb2245dc687a56a5adef9ad3fc675715803356fcfbd14168f93f22b67fac4c1 with x1, x2, x3 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
■ |
|