Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply set_ext with
d3786.. x0 (d3786.. x1 x2),
d3786.. (d3786.. x0 x1) x2 leaving 2 subgoals.
Apply unknownprop_ca91282e0ce9e0658e00929623a7308f21757843a59143f77f3c318bcf850a5e with
d3786.. x0 x1,
x2,
d3786.. x0 (d3786.. x1 x2) leaving 2 subgoals.
Apply unknownprop_ca91282e0ce9e0658e00929623a7308f21757843a59143f77f3c318bcf850a5e with
x0,
x1,
d3786.. x0 (d3786.. x1 x2) leaving 2 subgoals.
The subproof is completed by applying unknownprop_8f5bf12cfaed0ffd6b0b2703f40521e4f47dbe14ca71e17ebdcebdd96c630d67 with
x0,
d3786.. x1 x2.
Apply Subq_tra with
d3786.. x0 (d3786.. x1 x2),
d3786.. x1 x2,
x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_8c33f2993dbd85b3390e51467f1f34c3a7271a7424f5fa69403f3fe6fa095bed with
x0,
d3786.. x1 x2.
The subproof is completed by applying unknownprop_8f5bf12cfaed0ffd6b0b2703f40521e4f47dbe14ca71e17ebdcebdd96c630d67 with x1, x2.
Apply Subq_tra with
d3786.. x0 (d3786.. x1 x2),
d3786.. x1 x2,
x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_8c33f2993dbd85b3390e51467f1f34c3a7271a7424f5fa69403f3fe6fa095bed with
x0,
d3786.. x1 x2.
The subproof is completed by applying unknownprop_8c33f2993dbd85b3390e51467f1f34c3a7271a7424f5fa69403f3fe6fa095bed with x1, x2.
Apply unknownprop_ca91282e0ce9e0658e00929623a7308f21757843a59143f77f3c318bcf850a5e with
x0,
d3786.. x1 x2,
d3786.. (d3786.. x0 x1) x2 leaving 2 subgoals.
Apply Subq_tra with
d3786.. (d3786.. x0 x1) x2,
d3786.. x0 x1,
x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_8f5bf12cfaed0ffd6b0b2703f40521e4f47dbe14ca71e17ebdcebdd96c630d67 with
d3786.. x0 x1,
x2.
The subproof is completed by applying unknownprop_8f5bf12cfaed0ffd6b0b2703f40521e4f47dbe14ca71e17ebdcebdd96c630d67 with x0, x1.
Apply unknownprop_ca91282e0ce9e0658e00929623a7308f21757843a59143f77f3c318bcf850a5e with
x1,
x2,
d3786.. (d3786.. x0 x1) x2 leaving 2 subgoals.
Apply Subq_tra with
d3786.. (d3786.. x0 x1) x2,
d3786.. x0 x1,
x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_8f5bf12cfaed0ffd6b0b2703f40521e4f47dbe14ca71e17ebdcebdd96c630d67 with
d3786.. x0 x1,
x2.
The subproof is completed by applying unknownprop_8c33f2993dbd85b3390e51467f1f34c3a7271a7424f5fa69403f3fe6fa095bed with x0, x1.
The subproof is completed by applying unknownprop_8c33f2993dbd85b3390e51467f1f34c3a7271a7424f5fa69403f3fe6fa095bed with
d3786.. x0 x1,
x2.