Let x0 of type ι be given.
Apply cases_4 with
x0,
λ x1 . Church6_lt4p (nth_6_tuple x1) leaving 5 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_5e063b347ef5ac56a92183cc00c589df53087ab1e0b6353a236a973dc2f46966 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x2.
The subproof is completed by applying unknownprop_56ce56513a8af1327555b873c1c6ce07e295bb2d93a34f831bbfdb3328f2809b.
Apply unknownprop_487e017004ecabac0b8e518f0fcaf45b502b6f60f5af04ddefe015bde12eaf50 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x2.
The subproof is completed by applying unknownprop_995579645b8886904e46af0dc0ac8e19ee3cd4af7d78809ff698344ead396f5a.
Apply unknownprop_9205282ef77caa3eed787eb4fa460a34079ef649c9bf4aa55e938da8cedd6fa2 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x2.
The subproof is completed by applying unknownprop_bd8f81a1227d0cc25cea7c364f7541293f70705efd4999ad0dba8cf8857226a9.
Apply unknownprop_d77aca9102a0a7995bbfb825c57cbe3520e1f56683b5c476fb6c9389a8c86331 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . Church6_lt4p x2.
The subproof is completed by applying unknownprop_9ab406e767d5138f84eceb89ae815ef2f93656cc034576ca18ab84af7a608607.