Let x0 of type ι be given.
Let x1 of type (ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι) → ο be given.
Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with
permargs_i_2_3_0_1_4_5 (nth_6_tuple x0),
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι . x1 x3 x2.
Apply unknownprop_888d9bdc29aba745cfee3f27663169759486a003c9a4c811a668bb4e9c7cdcbb with
permargs_i_2_3_0_1_4_5 (nth_6_tuple x0).
Apply unknownprop_e4e4b3f2fb027bfa7e0d480fd7613c70f730d2ef7d2b0b335a19a8b751f04a2c with
nth_6_tuple x0.
Apply unknownprop_38a69925e68ff1a8dcf3a7f4e5069fa460ecf01c3c27215046eede1e2c2501a3 with
x0.
The subproof is completed by applying H0.