Let x0 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
binunion 0 x0,
x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with
0,
x0,
x1,
In x1 x0 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply FalseE with
In x1 x0.
Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with
x1.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with
0,
x0,
x1.
The subproof is completed by applying H0.