Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p (λ x2 x3 x4 x5 x6 x7 . permargs_i_2_3_0_1_4_5 x1 x2 x3 x4 x5 x7 x6) 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.
Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Apply H1 with
λ x1 : ι → ι → ι → ι → ι → ι → ι . ∀ x2 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x2 ⟶ Church6_lt4p (Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 x1 x2) leaving 6 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying unknownprop_e4e4b3f2fb027bfa7e0d480fd7613c70f730d2ef7d2b0b335a19a8b751f04a2c.
The subproof is completed by applying unknownprop_e4e4b3f2fb027bfa7e0d480fd7613c70f730d2ef7d2b0b335a19a8b751f04a2c.
The subproof is completed by applying L0.
The subproof is completed by applying unknownprop_e4e4b3f2fb027bfa7e0d480fd7613c70f730d2ef7d2b0b335a19a8b751f04a2c.
The subproof is completed by applying unknownprop_e4e4b3f2fb027bfa7e0d480fd7613c70f730d2ef7d2b0b335a19a8b751f04a2c.