Let x0 of type ι be given.
Apply unknownprop_136cc02be2eeb4eb60a56da6730dd8546fdf883c69bcebc5fc98beb801cd39e6 with
permargs_i_1_0_3_2_4_5 (nth_6_tuple x0).
Apply unknownprop_82a18ab52f7ac6281a607a1820c9620c483afb6be383087b7d72855319e580f5 with
nth_6_tuple x0.
Apply unknownprop_38a69925e68ff1a8dcf3a7f4e5069fa460ecf01c3c27215046eede1e2c2501a3 with
x0.
The subproof is completed by applying H0.