Let x0 of type ι → (ι → ο) → ο be given.
Assume H0:
∃ x1 . and (∃ x2 : ι → ο . x0 x1 x2) (∀ x2 x3 : ι → ο . x0 x1 x2 ⟶ x0 x1 x3 ⟶ x2 = x3).
Apply Eps_i_ex with
λ x1 . and (∃ x2 : ι → ο . x0 x1 x2) (∀ x2 x3 : ι → ο . x0 x1 x2 ⟶ x0 x1 x3 ⟶ x2 = x3).
The subproof is completed by applying H0.
Apply L1 with
x0 (DescrR_i_io_1 x0) (DescrR_i_io_2 x0).
Apply Descr_Vo1_prop with
λ x1 : ι → ο . x0 (DescrR_i_io_1 x0) x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.