Let x0 of type ι → ο be given.
Apply unknownprop_024cda690c1294bd6e6821da39a67e50f8a980f3aacf36d8a42158546a425719 with
λ x1 x2 : (ι → ο) → ο . x2 x0 ⟶ ∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x3 = x4.
The subproof is completed by applying unknownprop_896ccc9f209efa8a895211d65adb5a90348b419f100f6ab5e9762ce4d7fa9cc1 with ∃ x1 . x0 x1, ∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x1 = x2.