Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply setminusE with
u12,
u8,
x0,
x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_a36df829fd5ae696643b1cd180c001e7c72018b0aade2c8b02a3beb191bf4447 with
x0,
λ x2 . nIn x2 u8 ⟶ x1 x2 leaving 13 subgoals.
The subproof is completed by applying H5.
Apply FalseE with
x1 0.
Apply H6.
The subproof is completed by applying In_0_8.
Apply FalseE with
x1 u1.
Apply H6.
The subproof is completed by applying In_1_8.
Apply FalseE with
x1 u2.
Apply H6.
The subproof is completed by applying In_2_8.
Apply FalseE with
x1 u3.
Apply H6.
The subproof is completed by applying In_3_8.
Apply FalseE with
x1 u4.
Apply H6.
The subproof is completed by applying In_4_8.
Apply FalseE with
x1 u5.
Apply H6.
The subproof is completed by applying In_5_8.
Apply FalseE with
x1 u6.
Apply H6.
The subproof is completed by applying In_6_8.
Apply FalseE with
x1 u7.
Apply H6.
The subproof is completed by applying In_7_8.
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.