Let x0 of type ι be given.
Apply unknownprop_14e19ebc7e16f882d3be4482dbe497cecb7597969c9cae0a9f87fe87a0ee217a with
x0,
λ x1 . Church17_p (u17_to_Church17 x1) leaving 18 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_e6619adff47bbbf90a12e5475c1b155ebb1e2991a2d17411fd40e422e21ff562.
Apply unknownprop_f880a8473dab9f58d69fbf332c8547d500ca315e405258a93c99a34f8560efb6 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_93ed18843f4a06fdb1762e5b7fc89edc8da24a5d38de418508f9aca3fe120f8f.
Apply unknownprop_7c154441ca7b7a9fe09539322ad6531c3f48333c7018e2f8c866c0af44719d1a with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_233906471c2a36e258793125988364b5b4be5e26b5df943569d8a15ce4c97b59.
Apply unknownprop_50de3f92839624b98789d3fa24556e40d38a727836b3c2bd366269421355b28d with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_497df65ae9348f62989259dc92fffa35cd477d735ac36c17e9f5dc63bcd5da15.
Apply unknownprop_f6f6b2d4f503fb9b975e320862d0437f04a94f96cc19149de839c0a7d55394f3 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_aeac4ee3d08fd60f864a3d40a6422b2070323f5bdb4e126705e59ff4ccf8fa26.
Apply unknownprop_ccd09fc33db26fba17a1e8f5fd52159b676a35cf5706e2e445b9db64b4fc35c5 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_398a24facf4ebb42cf838f8cb0f1d64c4d83d480adfd36e0fa2e0b1bde52df48.
Apply unknownprop_b2c765c786aca76bfef751038ffbb16620c4c7136061de036517f3c71ce2abfd with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_8422ea19f7ca229a936fab0e3a1aadb25110b62375b34ff2715e426e6903f401.
Apply unknownprop_9d497d8c5ab47bb0417256780d394d93b6598b5e679bac7f2c3c702196ebcca4 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_d792dc995f6520052dfc965493173e3531c29f8140df360fa3c27b7268ed80b5.
Apply unknownprop_8f7d877f09ad2d2b6bd165b15d072d92366514d5c83c4caef2b25c48dd454e7b with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_c37600b80efb18922b2424c0ae3622d88c262b6e7e6fb3aa0f6bc2b0ba9f1be7.
Apply unknownprop_08c2582e457fa5da2b4ee2676b94e0e9b149b350b636df86eee53e8e8dded2c1 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_7fcbe5b61ad12e38a6853aaa6fe3dd0299d75fe061e77a480a4e344498540b83.
Apply unknownprop_c1a95e8160789154b1ae102566f570f1aea3813572fb362eeefeb21832fd0653 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_3de64cc15c614d92c317d5d39969a651d867528244eff253971f4e6ee88dced0.
Apply unknownprop_adf687ac5b6c91f712b3eb1ff0c482d096f763fa394d8ea395fcfe7d367eb8f2 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_6a85fd1fad00f32e7f8e46dd1246f3ab13554caed4c219f40087b53560da85b2.
Apply unknownprop_d33ea914c01284b1fc49147f7bcc51527f787dcf89c80cfdad2e5f419cbe1dbb with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_744a4c03b09434f04174e938301dc04f0c3f10e622d7fdbe408752834fe5b003.
Apply unknownprop_095d0670f988d22364f3d3b9681f2ca00bf954d60116baba131fbf1ee891de57 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_d664e656d766635177b954bb19d911f5792a5b476afc9d95f66c535e94450d07.
Apply unknownprop_c9b34bc382b6d599e61c555eac34a76c451754eb682c17d99a93f2a1e695d561 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_5749399996f8b07d8783c347f0cf6e04806eba2f6eba6fb3456b8e9db2686cda.
Apply unknownprop_e20cda3fec831e61f9db0bd6bee2791e26067278d174576042c0cb4b3ab479bb with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_9c9197f88eaab6add22634c2b7df334297862a6da7753d0d08affb6802924e7f.
Apply unknownprop_2491d2eab9fb9ff25fa0ab1839a83bd77980933cdf40d8cdd9120c539e464911 with
λ x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x2.
The subproof is completed by applying unknownprop_65d5ff984a67d49c14142f780ead671595b0d7535fbc96a800a59481ec6515c0.