Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p (permargs_i_2_3_0_1_4_5 x1) leaving 4 subgoals.
The subproof is completed by applying unknownprop_bd8f81a1227d0cc25cea7c364f7541293f70705efd4999ad0dba8cf8857226a9.
The subproof is completed by applying unknownprop_9ab406e767d5138f84eceb89ae815ef2f93656cc034576ca18ab84af7a608607.
The subproof is completed by applying unknownprop_56ce56513a8af1327555b873c1c6ce07e295bb2d93a34f831bbfdb3328f2809b.
The subproof is completed by applying unknownprop_995579645b8886904e46af0dc0ac8e19ee3cd4af7d78809ff698344ead396f5a.