Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with
x2,
setminus x0 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_3fe7f97dcb00bcf31cf989081bd8403f8f0647acc7dd719f8a7da64cd4837dac with
x0,
x1,
x2 leaving 2 subgoals.
Apply unknownprop_75b5762e65badae8f9531d40fddd332ff95b59f608d93c7a55f19f4fa5ef37d5 with
x2,
x0.
The subproof is completed by applying H1.
Apply unknownprop_b30a94f49240f0717f4ecb200a605aa8a4e6dad6dc5d1afa60c37866ee96baab with
x2,
x1.
The subproof is completed by applying H2.