Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x1 ⊆ x0.
Apply binunion_com with
setminus x0 x1,
x1,
λ x2 x3 . x0 = x3.
Apply unknownprop_ff7563d54b310a61c1a752018a571ea929b537103802faa76e16375d0d762c34 with
x1,
x0.
The subproof is completed by applying H0.