Let x0 of type ι be given.
Apply unknownprop_f0f6d6a5e0bad31ef814582844f5581ef6b06897d8b34d179a5f11d6a4ff9407 with
x0,
λ x1 x2 . x1 ∈ u4 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_ad1ff34c5887c7a56d642b3b98792cc3a70431e3d05f920a54296dac440cbedc with
u17_to_Church17 x0.
The subproof is completed by applying H1.