Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply setminusE with
u18,
u12,
x0,
x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ordsuccE with
u17,
x0,
x1 x0 leaving 3 subgoals.
The subproof is completed by applying H7.
Apply unknownprop_d2eb1da8f945e97882f3b17888a7fe6e441c3a4b20ad156ba00c22e721803915 with
x0,
x1 leaving 6 subgoals.
Apply setminusI with
u17,
u12,
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.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply H9 with
λ x2 x3 . x1 x3.
The subproof is completed by applying H6.