Let x0 of type ι be given.
Apply unknownprop_a36df829fd5ae696643b1cd180c001e7c72018b0aade2c8b02a3beb191bf4447 with
x0,
λ x1 . u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x1 ∈ u12 leaving 13 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645 with
λ x1 x2 . x2 ∈ u12.
The subproof is completed by applying unknownprop_b1b74a38cb206cf70f2e2bbc4ccd3cbdbf8c8df3defd64ff8c8a7258b3a2047a.
Apply unknownprop_3ce04bff2a395cf5fe0b94d0636cc8dbea0e46272d1360d7109558a625b43849 with
λ x1 x2 . x2 ∈ u12.
The subproof is completed by applying unknownprop_cf5ceb5c8b16071a67f4b018bbc8955118e3633f8bcf650790850107ad2027ee.
Apply unknownprop_5f23a09617e395d3412bcd886825a830fcbca9dbfaa3bb762a6b0286bbba2699 with
λ x1 x2 . x2 ∈ u12.
The subproof is completed by applying unknownprop_a2ef0c58cfd090f3c9e6e7916f6b56032d6bdd4de509aa9fb32f7308f99daf5a.
Apply unknownprop_2deda5cc0874f100e0fcd31fbab30140488390c1e46b9b2da484e79975ce6ae8 with
λ x1 x2 . x2 ∈ u12.
The subproof is completed by applying unknownprop_987ba5536dee4e8ff190eaeed4d2bb3ab5d85c45e6623acb29ce14f019a19681.
Apply unknownprop_d02d672c88891239a2034f8db0a8f9c766e8b44a6127d48b08a622cce7dc65fa with
λ x1 x2 . x2 ∈ u12.
The subproof is completed by applying unknownprop_75d836f404cbbeae78f524a2ea7f26282023039d9accd25589aa1c1720bb8121.
Apply unknownprop_b4b0b30bf8e5ff91ed4869311536b86e18ba1e4d9dcdabf73d46693ed9a5b67b with
λ x1 x2 . x2 ∈ u12.
The subproof is completed by applying unknownprop_a31357c4255c39823e518ff3fc8fa06c75e6252111ceae22b3d4f1c89a01d10b.
Apply unknownprop_8a85de05c64795068871a87d3b06ba1e5395c94812285b09588df3e01a1e0ea3 with
λ x1 x2 . x2 ∈ u12.
The subproof is completed by applying unknownprop_4fce167ccdcc7fb45429dcf8a3db15dc462c457fe760841310c58bc94a706ed3.
Apply unknownprop_c0eb4e3448ef31f6408883194d369de2b67b2c3b8eb9ad88a4d52d9ee850a560 with
λ x1 x2 . x2 ∈ u12.
The subproof is completed by applying unknownprop_73e4e62694bfb193433658c654297b6ed3eb985937a9e426b510b83e68de24d1.
Apply unknownprop_f74f5074ad12d57b1f85300d32210524157b09a0919ee38128acf015331c35f0 with
λ x1 x2 . x2 ∈ u12.
The subproof is completed by applying unknownprop_e58cb2c6f977d1b0d5350ed902991ead1b80327bc1b160612a3fd1cd20c9fd3b.
Apply unknownprop_4e46240fa21fb39b84708f415e3b21cc616773a08b926976627048ab8fc29078 with
λ x1 x2 . x2 ∈ u12.
The subproof is completed by applying unknownprop_89f074e5696e72c1d0b8f6c7a30d07f4920551bfce89ff386ae0ecf5a82d48e4.
Apply unknownprop_29ccb5c4e7950928d647b0941425c5e64d69ebaaed74cba3c055174a14ae4c5b with
λ x1 x2 . x2 ∈ u12.
The subproof is completed by applying unknownprop_2e87f3f906df12d03519748b94abd9f72cc673eb197d25aaf167a3737a0cc14b.
Apply unknownprop_9b334a439f93d75505077dcc1fe4c60157a3105589338dee138085e931431815 with
λ x1 x2 . x2 ∈ u12.
The subproof is completed by applying unknownprop_2453a2b3484043c8ce568faca0a1096a3c2d75e863532a7d5d6a9f964c17a76f.