Apply Empty_eq with
prim3 0.
Let x0 of type ι be given.
Apply UnionE with
0,
x0,
False leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H1:
and (x0 ∈ x1) (x1 ∈ 0).
Apply EmptyE with
x1.
Apply andER with
x0 ∈ x1,
x1 ∈ 0.
The subproof is completed by applying H1.