Let R be given.

Assume H1: ∃x, (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z).

We prove the intermediate claim L1: (∃y : set → prop, R (DescrR_i_io_1 R) y) ∧ (∀y z : set → prop, R (DescrR_i_io_1 R) y → R (DescrR_i_io_1 R) z → y = z).

An exact proof term for the current goal is (Eps_i_ex (λx ⇒ (∃y : set → prop, R x y) ∧ (∀y z : set → prop, R x y → R x z → y = z)) H1).

Apply L1 to the current goal.

Assume H2 H3.

An exact proof term for the current goal is Descr_Vo1_prop (λy ⇒ R (DescrR_i_io_1 R) y) H2 H3.

∎