Let x0 of type ι be given.
Apply unknownprop_a23ec6a55ac212526d74cbf0d04096929ad453b0eb0f8023e32b8a33930d39fb with
setminus x0 0,
x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_b22f3f2b1b7fbab88f43a774dccf5e91ed22477d6a539a7e1f7cbd5b32ba5400 with x0, 0.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
x0,
setminus x0 0.
Let x1 of type ι be given.
Apply unknownprop_3fe7f97dcb00bcf31cf989081bd8403f8f0647acc7dd719f8a7da64cd4837dac with
x0,
0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_17472844d8aa5bafba99fcc9fb4ab7cb63948fdebc0c0bd6923258911ef1e72c with x1.