Apply unknownprop_b2c765c786aca76bfef751038ffbb16620c4c7136061de036517f3c71ce2abfd 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) = u4.

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 . x7))) u4.

The subproof is completed by applying H0.

■

Proofgold Proof