Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
binunion x0 x1,
binunion x1 x0.
Let x2 of type ι be given.
Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with
x0,
x1,
x2,
In x2 (binunion x1 x0) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with
x1,
x0,
x2.
The subproof is completed by applying H1.
Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with
x1,
x0,
x2.
The subproof is completed by applying H1.