Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p (λ x2 x3 x4 x5 x6 x7 . permargs_i_3_2_1_0_4_5 x1 x2 x3 x4 x5 x7 x6) leaving 4 subgoals.
The subproof is completed by applying unknownprop_9ab406e767d5138f84eceb89ae815ef2f93656cc034576ca18ab84af7a608607.
The subproof is completed by applying unknownprop_bd8f81a1227d0cc25cea7c364f7541293f70705efd4999ad0dba8cf8857226a9.
The subproof is completed by applying unknownprop_995579645b8886904e46af0dc0ac8e19ee3cd4af7d78809ff698344ead396f5a.
The subproof is completed by applying unknownprop_56ce56513a8af1327555b873c1c6ce07e295bb2d93a34f831bbfdb3328f2809b.
Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply H1 with
λ x1 : ι → ι → ι → ι → ι → ι → ι . ∀ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x2 ⟶ Church6_lt4p (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x1 x2) leaving 6 subgoals.
The subproof is completed by applying unknownprop_03dd63d746fcacdd2139f1b753227929c56f1868867976a2dfb9db401b403f8a.
The subproof is completed by applying L0.
The subproof is completed by applying L0.
The subproof is completed by applying unknownprop_03dd63d746fcacdd2139f1b753227929c56f1868867976a2dfb9db401b403f8a.
The subproof is completed by applying L0.
The subproof is completed by applying unknownprop_03dd63d746fcacdd2139f1b753227929c56f1868867976a2dfb9db401b403f8a.