Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply setminusE with
u16,
u12,
x0,
x1 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_485b5a544f4a752392d62c01e55a5e36a8748d64fd7af6f27349bd2453284446 with
x0,
λ x2 . nIn x2 u12 ⟶ x1 x2 leaving 17 subgoals.
The subproof is completed by applying H5.
Apply FalseE with
x1 0.
Apply H6.
The subproof is completed by applying unknownprop_a2ef0c58cfd090f3c9e6e7916f6b56032d6bdd4de509aa9fb32f7308f99daf5a.
Apply FalseE with
x1 u1.
Apply H6.
The subproof is completed by applying unknownprop_b1b74a38cb206cf70f2e2bbc4ccd3cbdbf8c8df3defd64ff8c8a7258b3a2047a.
Apply FalseE with
x1 u2.
Apply H6.
The subproof is completed by applying unknownprop_987ba5536dee4e8ff190eaeed4d2bb3ab5d85c45e6623acb29ce14f019a19681.
Apply FalseE with
x1 u3.
Apply H6.
The subproof is completed by applying unknownprop_cf5ceb5c8b16071a67f4b018bbc8955118e3633f8bcf650790850107ad2027ee.
Apply FalseE with
x1 u4.
Apply H6.
The subproof is completed by applying unknownprop_4fce167ccdcc7fb45429dcf8a3db15dc462c457fe760841310c58bc94a706ed3.
Apply FalseE with
x1 u5.
Apply H6.
The subproof is completed by applying unknownprop_75d836f404cbbeae78f524a2ea7f26282023039d9accd25589aa1c1720bb8121.
Apply FalseE with
x1 u6.
Apply H6.
The subproof is completed by applying unknownprop_73e4e62694bfb193433658c654297b6ed3eb985937a9e426b510b83e68de24d1.
Apply FalseE with
x1 u7.
Apply H6.
The subproof is completed by applying unknownprop_a31357c4255c39823e518ff3fc8fa06c75e6252111ceae22b3d4f1c89a01d10b.
Apply FalseE with
x1 u8.
Apply H6.
The subproof is completed by applying unknownprop_89f074e5696e72c1d0b8f6c7a30d07f4920551bfce89ff386ae0ecf5a82d48e4.
Apply FalseE with
x1 u9.
Apply H6.
The subproof is completed by applying unknownprop_2453a2b3484043c8ce568faca0a1096a3c2d75e863532a7d5d6a9f964c17a76f.
Apply FalseE with
x1 u10.
Apply H6.
The subproof is completed by applying unknownprop_e58cb2c6f977d1b0d5350ed902991ead1b80327bc1b160612a3fd1cd20c9fd3b.
Apply FalseE with
x1 u11.
Apply H6.
The subproof is completed by applying unknownprop_2e87f3f906df12d03519748b94abd9f72cc673eb197d25aaf167a3737a0cc14b.
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.