Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_969020ecc80c532d1b1becba35b6297793bf495fb82300936c8a1e4e62750e6f 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.