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