Let x0 of type ι be given.
Apply cases_6 with
x0,
λ x1 . Church17_lt6 (u17_to_Church17 x1) leaving 7 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt6 x2.
The subproof is completed by applying unknownprop_d1a3c19b0809c443bbe0c4c68ad56576b3afdf87e4e7fbf2c2f7269e057a7955.
Apply unknownprop_f880a8473dab9f58d69fbf332c8547d500ca315e405258a93c99a34f8560efb6 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt6 x2.
The subproof is completed by applying unknownprop_6489c310e4092415a7add1ef23a8ab65d3db0cf2b528972b24e4fa2dc350de02.
Apply unknownprop_7c154441ca7b7a9fe09539322ad6531c3f48333c7018e2f8c866c0af44719d1a with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt6 x2.
The subproof is completed by applying unknownprop_3e6043e725e380c7f2e40e2120ea8935fc15a89033cb0844a94d8e43b2b72a17.
Apply unknownprop_50de3f92839624b98789d3fa24556e40d38a727836b3c2bd366269421355b28d with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt6 x2.
The subproof is completed by applying unknownprop_e79484dcbf874420cf565fdcf844a925a966f9d983bf7da6208ee336a5cb1e30.
Apply unknownprop_f6f6b2d4f503fb9b975e320862d0437f04a94f96cc19149de839c0a7d55394f3 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt6 x2.
The subproof is completed by applying unknownprop_0ff8567e050fe592c65522f7e71b1f2de1c0b257e4f6ba6818d96245ea1f56fd.
Apply unknownprop_ccd09fc33db26fba17a1e8f5fd52159b676a35cf5706e2e445b9db64b4fc35c5 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_lt6 x2.
The subproof is completed by applying unknownprop_b55ff672d4d1667b0d11d0c5ed88baec2813fe2de5f19c48110a4ffec662d01e.