Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p (Church17_perm_1_2_3_4_5_6_7_8_9_10_11_12_13_14_15_16_0 x1) leaving 17 subgoals.
The subproof is completed by applying unknownprop_93ed18843f4a06fdb1762e5b7fc89edc8da24a5d38de418508f9aca3fe120f8f.
The subproof is completed by applying unknownprop_233906471c2a36e258793125988364b5b4be5e26b5df943569d8a15ce4c97b59.
The subproof is completed by applying unknownprop_497df65ae9348f62989259dc92fffa35cd477d735ac36c17e9f5dc63bcd5da15.
The subproof is completed by applying unknownprop_aeac4ee3d08fd60f864a3d40a6422b2070323f5bdb4e126705e59ff4ccf8fa26.
The subproof is completed by applying unknownprop_398a24facf4ebb42cf838f8cb0f1d64c4d83d480adfd36e0fa2e0b1bde52df48.
The subproof is completed by applying unknownprop_8422ea19f7ca229a936fab0e3a1aadb25110b62375b34ff2715e426e6903f401.
The subproof is completed by applying unknownprop_d792dc995f6520052dfc965493173e3531c29f8140df360fa3c27b7268ed80b5.
The subproof is completed by applying unknownprop_c37600b80efb18922b2424c0ae3622d88c262b6e7e6fb3aa0f6bc2b0ba9f1be7.
The subproof is completed by applying unknownprop_7fcbe5b61ad12e38a6853aaa6fe3dd0299d75fe061e77a480a4e344498540b83.
The subproof is completed by applying unknownprop_3de64cc15c614d92c317d5d39969a651d867528244eff253971f4e6ee88dced0.
The subproof is completed by applying unknownprop_6a85fd1fad00f32e7f8e46dd1246f3ab13554caed4c219f40087b53560da85b2.
The subproof is completed by applying unknownprop_744a4c03b09434f04174e938301dc04f0c3f10e622d7fdbe408752834fe5b003.
The subproof is completed by applying unknownprop_d664e656d766635177b954bb19d911f5792a5b476afc9d95f66c535e94450d07.
The subproof is completed by applying unknownprop_5749399996f8b07d8783c347f0cf6e04806eba2f6eba6fb3456b8e9db2686cda.
The subproof is completed by applying unknownprop_9c9197f88eaab6add22634c2b7df334297862a6da7753d0d08affb6802924e7f.
The subproof is completed by applying unknownprop_65d5ff984a67d49c14142f780ead671595b0d7535fbc96a800a59481ec6515c0.
The subproof is completed by applying unknownprop_e6619adff47bbbf90a12e5475c1b155ebb1e2991a2d17411fd40e422e21ff562.