Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply Eps_i_ex with
λ x2 . ∀ x3 . iff (prim1 x3 x2) (and (prim1 x3 x0) (x1 x3)).
The subproof is completed by applying unknownprop_73dbb39494df6eeccf6ebcf4dc59ad557f592acdc48fe63aaaaa197f2f3a353f with x0, x1.