Let x0 of type ι be given.
Apply cases_4 with
x0,
λ x1 . 84660.. (u17_to_Church17 x1) leaving 5 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 84660.. x2.
The subproof is completed by applying unknownprop_9fed24c88e6ce3e597374a5d5c30c1890e6b13f7a8199e5fc326710ee4a0c30c.
Apply unknownprop_f880a8473dab9f58d69fbf332c8547d500ca315e405258a93c99a34f8560efb6 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 84660.. x2.
The subproof is completed by applying unknownprop_6918a53d27da09499b369f7f0ade3a5e248b2b30741c201909c7c83656907b69.
Apply unknownprop_7c154441ca7b7a9fe09539322ad6531c3f48333c7018e2f8c866c0af44719d1a with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 84660.. x2.
The subproof is completed by applying unknownprop_c920acd68bacde16f7e610e45bdd38ba97d3c9be38ca3b5d26872fe4b54e66af.
Apply unknownprop_50de3f92839624b98789d3fa24556e40d38a727836b3c2bd366269421355b28d with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 84660.. x2.
The subproof is completed by applying unknownprop_0d64c67c0d955bbbf1056696bccf837580fc127a9100042c9fc9336f314a191e.