Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply setminusE with
u22,
u17,
x0,
x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_d063ce03105999ee16bbafa5f65220ff2535b43f3c3d0afd7d320f4f3006227c with
x0,
λ x2 . nIn x2 u17 ⟶ x1 x2 leaving 23 subgoals.
The subproof is completed by applying H6.
Apply FalseE with
x1 0.
Apply H7.
The subproof is completed by applying unknownprop_9851dfe301262128a9dc5def6f083cbb499c4d0eace7612e5dc050c4fe5ba3c7.
Apply FalseE with
x1 u1.
Apply H7.
The subproof is completed by applying unknownprop_4f0f2f2c8505addb4aa66d1187553d1cf0a291464cc87b78a3faaf7ae73ed155.
Apply FalseE with
x1 u2.
Apply H7.
The subproof is completed by applying unknownprop_fcb0372c2816a1d869a174f57c9ee90635b20300695b8cc5b4a5ca8436427e30.
Apply FalseE with
x1 u3.
Apply H7.
The subproof is completed by applying unknownprop_515e04c9d20f4760fa1f9ec9f7d43a79e2cf83cd96ac9929a00f63e10a33bee6.
Apply FalseE with
x1 u4.
Apply H7.
The subproof is completed by applying unknownprop_8bfb0eb80a8f5f9fa400351ad533eb8f6abcbab81f79751d9b99dc5c5b198b37.
Apply FalseE with
x1 u5.
Apply H7.
The subproof is completed by applying unknownprop_add6307eacf71a9b26cddaf6256b63e565e929785d0ee0946ee6b253d6c3852e.
Apply FalseE with
x1 u6.
Apply H7.
The subproof is completed by applying unknownprop_e8645556daad09b81c208e8cbf014ff23194c321a76d028c3b35a1714720baab.
Apply FalseE with
x1 u7.
Apply H7.
The subproof is completed by applying unknownprop_97cf1bf10df747733c6e7166825443492e8a9bbd5381654e4874ef5f3ceacd0a.
Apply FalseE with
x1 u8.
Apply H7.
The subproof is completed by applying unknownprop_6e6799a9f21ccdffe58af218db8306610bd1441f3fa0fcc3f6eaa957ce165f57.
Apply FalseE with
x1 u9.
Apply H7.
The subproof is completed by applying unknownprop_abbef1301044c000653f42960a8047881f2ef656bd9cecef0ae9b764b6c0784f.
Apply FalseE with
x1 u10.
Apply H7.
The subproof is completed by applying unknownprop_7af243686256d97349e2c2a55c958e2d435fe9a5e016344b19465fce23ad5676.
Apply FalseE with
x1 u11.
Apply H7.
The subproof is completed by applying unknownprop_fde6379bebd0b99b66d966901300c529916d83c8c1f209841f486bb2568cf012.
Apply FalseE with
x1 u12.
Apply H7.
The subproof is completed by applying unknownprop_b7a4a37161804b376f25028de76b0714142123cbd842ba90c86afe8baa6a8a9e.
Apply FalseE with
x1 u13.
Apply H7.
The subproof is completed by applying unknownprop_ee249701bfbf4a0ddc5825c1bc6fff36b37e7d1af2b7d307fdfcf229c66eb3d7.
Apply FalseE with
x1 u14.
Apply H7.
The subproof is completed by applying unknownprop_19ecd6ac8599e49ad47f95e5b1703b05d2332ac49ec04a48785748b0d8a5094a.
Apply FalseE with
x1 u15.
Apply H7.
The subproof is completed by applying unknownprop_35f4d337254964d13bfee3413f1b56f908aee5828cc15d13f416e7a488640c53.
Apply FalseE with
x1 u16.
Apply H7.
The subproof is completed by applying unknownprop_a76efb72f36a26d5f27a9b9224b42b8be1785c9e1b5b0390f7ccb72d2b130266.
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.