Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply set_ext with
1ad11.. x0 (d3786.. x1 x2),
0ac37.. (1ad11.. x0 x1) (1ad11.. x0 x2) leaving 2 subgoals.
Let x3 of type ι be given.
Apply unknownprop_b29d0d66991b8737c3ef6109cea8b8736c6edd642ea721f35cfa04fecdda0905 with
x0,
d3786.. x1 x2,
x3,
prim1 x3 (0ac37.. (1ad11.. x0 x1) (1ad11.. x0 x2)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply dneg with
prim1 x3 (0ac37.. (1ad11.. x0 x1) (1ad11.. x0 x2)).
Apply H2.
Apply unknownprop_0eb2245dc687a56a5adef9ad3fc675715803356fcfbd14168f93f22b67fac4c1 with
x1,
x2,
x3 leaving 2 subgoals.
Apply dneg with
prim1 x3 x1.
Apply H3.
Apply unknownprop_0b5b61a66a1ed2eb843dbce5c5f6930c63a284fe5e33704d9f0cc564310ec40b with
1ad11.. x0 x1,
1ad11.. x0 x2,
x3.
Apply unknownprop_4469442df960b88f16925ae745a59dde3c3d26a1d7b003702e92e0a7ea2361ef with
x0,
x1,
x3 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
Apply dneg with
prim1 x3 x2.
Apply H3.
Apply unknownprop_e4d6e0bfb4ef6d52ee13edd54a77c8cc7f0a3af8ffb1b8da66d4f98842dd28b5 with
1ad11.. x0 x1,
1ad11.. x0 x2,
x3.
Apply unknownprop_4469442df960b88f16925ae745a59dde3c3d26a1d7b003702e92e0a7ea2361ef with
x0,
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
Apply unknownprop_c16c0737d29e3b3e820cf0e7f73a8868a90e8434c78c164566097cca1a566416 with
1ad11.. x0 x1,
1ad11.. x0 x2,
1ad11.. x0 (d3786.. x1 x2) leaving 2 subgoals.
Apply unknownprop_0602300724abfe8d2c6bf46afb7f4c8fc3acf346ac0b3d551c62bcf7339c23d3 with
x0,
x1,
d3786.. x1 x2.
The subproof is completed by applying unknownprop_8f5bf12cfaed0ffd6b0b2703f40521e4f47dbe14ca71e17ebdcebdd96c630d67 with x1, x2.
Apply unknownprop_0602300724abfe8d2c6bf46afb7f4c8fc3acf346ac0b3d551c62bcf7339c23d3 with
x0,
x2,
d3786.. x1 x2.
The subproof is completed by applying unknownprop_8c33f2993dbd85b3390e51467f1f34c3a7271a7424f5fa69403f3fe6fa095bed with x1, x2.