Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply setminusE with
u16,
u10,
x0,
x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply xm with
x0 ∈ u12,
x1 x0 leaving 2 subgoals.
Apply unknownprop_fe3434c13e4d9f957110bf39b27112a1224a05dbf0d1a39a1c9cb87663b7ee08 with
x0,
x1 leaving 3 subgoals.
Apply setminusI with
u12,
u10,
x0 leaving 2 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H8.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_bf17ea03608bec2ab1db40555d0b2aea03020efffda1ccd3dabfc161366b81c8 with
x0,
x1 leaving 5 subgoals.
Apply setminusI with
u16,
u12,
x0 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H9.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.