Apply unknownprop_6d01d49ea450d3e472df52e27a7b74861b461083d49142b218ad17a5e9f7fa4b with
u17_to_Church17 leaving 17 subgoals.
The subproof is completed by applying unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd.
The subproof is completed by applying unknownprop_f880a8473dab9f58d69fbf332c8547d500ca315e405258a93c99a34f8560efb6.
The subproof is completed by applying unknownprop_7c154441ca7b7a9fe09539322ad6531c3f48333c7018e2f8c866c0af44719d1a.
The subproof is completed by applying unknownprop_50de3f92839624b98789d3fa24556e40d38a727836b3c2bd366269421355b28d.
The subproof is completed by applying unknownprop_f6f6b2d4f503fb9b975e320862d0437f04a94f96cc19149de839c0a7d55394f3.
The subproof is completed by applying unknownprop_ccd09fc33db26fba17a1e8f5fd52159b676a35cf5706e2e445b9db64b4fc35c5.
The subproof is completed by applying unknownprop_b2c765c786aca76bfef751038ffbb16620c4c7136061de036517f3c71ce2abfd.
The subproof is completed by applying unknownprop_9d497d8c5ab47bb0417256780d394d93b6598b5e679bac7f2c3c702196ebcca4.
The subproof is completed by applying unknownprop_8f7d877f09ad2d2b6bd165b15d072d92366514d5c83c4caef2b25c48dd454e7b.
The subproof is completed by applying unknownprop_08c2582e457fa5da2b4ee2676b94e0e9b149b350b636df86eee53e8e8dded2c1.
The subproof is completed by applying unknownprop_c1a95e8160789154b1ae102566f570f1aea3813572fb362eeefeb21832fd0653.
The subproof is completed by applying unknownprop_adf687ac5b6c91f712b3eb1ff0c482d096f763fa394d8ea395fcfe7d367eb8f2.
The subproof is completed by applying unknownprop_d33ea914c01284b1fc49147f7bcc51527f787dcf89c80cfdad2e5f419cbe1dbb.
The subproof is completed by applying unknownprop_095d0670f988d22364f3d3b9681f2ca00bf954d60116baba131fbf1ee891de57.
The subproof is completed by applying unknownprop_c9b34bc382b6d599e61c555eac34a76c451754eb682c17d99a93f2a1e695d561.
The subproof is completed by applying unknownprop_e20cda3fec831e61f9db0bd6bee2791e26067278d174576042c0cb4b3ab479bb.
The subproof is completed by applying unknownprop_2491d2eab9fb9ff25fa0ab1839a83bd77980933cdf40d8cdd9120c539e464911.