Apply unknownprop_095d0670f988d22364f3d3b9681f2ca00bf954d60116baba131fbf1ee891de57 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) = u14.

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 . x14))) u14.

The subproof is completed by applying H0.

■

Proofgold Proof