Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply notE with
In x1 (Union x0) leaving 2 subgoals.
Apply unknownprop_9bccc16873f624a3c3c071d170820d76e64a5491b15f0c2f0287b0026ecb19b8 with
x1,
Union x0.
The subproof is completed by applying H0.
Apply unknownprop_bb7319fda7123d5f775b6b29aaea60dee8b8450dbda3fb13de42ee7deaa111d5 with
x0,
x1,
x2 leaving 2 subgoals.
Apply unknownprop_75b5762e65badae8f9531d40fddd332ff95b59f608d93c7a55f19f4fa5ef37d5 with
x1,
x2.
The subproof is completed by applying H1.
Apply unknownprop_75b5762e65badae8f9531d40fddd332ff95b59f608d93c7a55f19f4fa5ef37d5 with
x2,
x0.
The subproof is completed by applying H2.