Apply unknownprop_ccd09fc33db26fba17a1e8f5fd52159b676a35cf5706e2e445b9db64b4fc35c5 with λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_to_u17 (Church17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x1) = u7.

Let x0 of type ι → ι → ο be given.

Assume H0: x0 (Church17_to_u17 (Church17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x6))) u7.

The subproof is completed by applying H0.

■

Proofgold Proof