Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply setminusE with
u17,
u12,
x0,
x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ordsuccE with
u16,
x0,
x1 x0 leaving 3 subgoals.
The subproof is completed by applying H6.
Apply unknownprop_bf17ea03608bec2ab1db40555d0b2aea03020efffda1ccd3dabfc161366b81c8 with
x0,
x1 leaving 5 subgoals.
Apply setminusI with
u16,
u12,
x0 leaving 2 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H7.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply H8 with
λ x2 x3 . x1 x3.
The subproof is completed by applying H5.