Let x0 of type ι be given.
Apply cases_8 with
x0,
λ x1 . u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x1 ∈ u8 leaving 9 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645 with
λ x1 x2 . x2 ∈ u8.
The subproof is completed by applying In_1_8.
Apply unknownprop_3ce04bff2a395cf5fe0b94d0636cc8dbea0e46272d1360d7109558a625b43849 with
λ x1 x2 . x2 ∈ u8.
The subproof is completed by applying In_3_8.
Apply unknownprop_5f23a09617e395d3412bcd886825a830fcbca9dbfaa3bb762a6b0286bbba2699 with
λ x1 x2 . x2 ∈ u8.
The subproof is completed by applying In_0_8.
Apply unknownprop_2deda5cc0874f100e0fcd31fbab30140488390c1e46b9b2da484e79975ce6ae8 with
λ x1 x2 . x2 ∈ u8.
The subproof is completed by applying In_2_8.
Apply unknownprop_d02d672c88891239a2034f8db0a8f9c766e8b44a6127d48b08a622cce7dc65fa with
λ x1 x2 . x2 ∈ u8.
The subproof is completed by applying In_5_8.
Apply unknownprop_b4b0b30bf8e5ff91ed4869311536b86e18ba1e4d9dcdabf73d46693ed9a5b67b with
λ x1 x2 . x2 ∈ u8.
The subproof is completed by applying In_7_8.
Apply unknownprop_8a85de05c64795068871a87d3b06ba1e5395c94812285b09588df3e01a1e0ea3 with
λ x1 x2 . x2 ∈ u8.
The subproof is completed by applying In_4_8.
Apply unknownprop_c0eb4e3448ef31f6408883194d369de2b67b2c3b8eb9ad88a4d52d9ee850a560 with
λ x1 x2 . x2 ∈ u8.
The subproof is completed by applying In_6_8.