Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply setminusE with
u12,
u10,
x0,
x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply ordsuccE with
u11,
x0,
x1 x0 leaving 3 subgoals.
The subproof is completed by applying H3.
Apply ordsuccE with
u10,
x0,
x1 x0 leaving 3 subgoals.
The subproof is completed by applying H5.
Apply FalseE with
x1 x0.
Apply H4.
The subproof is completed by applying H6.
Apply H6 with
λ x2 x3 . x1 x3.
The subproof is completed by applying H1.
Apply H5 with
λ x2 x3 . x1 x3.
The subproof is completed by applying H2.