Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.
Apply H0 with
λ x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p (Church13_perm_5_6_7_8_9_10_11_12_0_1_2_3_4 x1) leaving 13 subgoals.
The subproof is completed by applying unknownprop_2275c30730a86a8b5e92c69a3cf62226cb91c94f842745d885aae952e4aec475.
The subproof is completed by applying unknownprop_af2a1b54824c0bcac106e306823cdf745ddadb1cb4ff3d16a82269625fefc7d4.
The subproof is completed by applying unknownprop_596dfb802632adb73ea48164c53a57c30f1012fe27955d11686758a101b7149d.
The subproof is completed by applying unknownprop_50472d7abd1881ae03e9d8bb4157df2bf5b1683170237a2acc8397347adcb4f4.
The subproof is completed by applying unknownprop_1f56b45f0c7c3bae8d2fefe625ddc5f2e352f95a05bc1ddcbe2a1e6319b2efb1.
The subproof is completed by applying unknownprop_1705677bb2891af01232540762f936ba15268cba2c18878c91db2fc6b9de2c54.
The subproof is completed by applying unknownprop_1b90f1280b68f731b1e6847827f5b51bc26aad732250097484d79ba832396c44.
The subproof is completed by applying unknownprop_ed489a2212f16ff8acf2018142cb5229cb5c399f8206cf8e20e508de6a09ab2c.
The subproof is completed by applying unknownprop_a619d41e7dd73fd2fd7a22e345cc585bca94f0a556dabdde7ba613d280fc1bb9.
The subproof is completed by applying unknownprop_56e5b078b135657df6b920f8c41633bbbc869255cbf04817b1c0569e953798ea.
The subproof is completed by applying unknownprop_64a05e04ff07f2333eab12fcce0b713bfb051cbbce19306572d78b255c2f5222.
The subproof is completed by applying unknownprop_ccf2dc8baa5a60239d2b334119b91cb320d200e197fef0daa6705ddcacfec32a.
The subproof is completed by applying unknownprop_ec3bfa3241ab3c5244e2af2ff034529622ae6db8f50ffa68a44651955e5adb06.