Apply unknownprop_18c079d0a948e2707cbd31a4293ae2dc77179c2184f0225dd81bf201082f253d with
u17_to_Church17,
u8,
λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8.
The subproof is completed by applying unknownprop_27bc12f3788ce8c72d6c4ccb1a7a7f2ccd75e6f44a01c5ed4eeb6b64187d9eed.