Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_ee5e0fe730eedc37f764400300b0ed7a640b3bede985cf7ccb67403eb532be1a with
u17_to_Church17 x1,
u17_to_Church17 x0,
λ x2 x3 : ι → ι → ι . x3 = λ x4 x5 . x4 leaving 3 subgoals.
Apply unknownprop_f44342ed74648c23c8734d945bc8b2c1af5a9cb594ef51477e7844cb71f944f8 with
x1.
The subproof is completed by applying H1.
Apply unknownprop_f44342ed74648c23c8734d945bc8b2c1af5a9cb594ef51477e7844cb71f944f8 with
x0.
The subproof is completed by applying H2.
Apply H0 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.