Apply Pex to the current goal.
Let f be given.
Assume Hf: P f.
We prove the intermediate claim L1: f = Descr_Vo1.
Apply func_ext set prop to the current goal.
Let x be given.
We will prove f x = Descr_Vo1 x.
Apply prop_ext_2 to the current goal.
Assume H1: f x.
Let h be given.
Assume Hh: P h.
We will prove h x.
rewrite the current goal using Puniq f h Hf Hh (from right to left).
An exact proof term for the current goal is H1.
Assume H1: Descr_Vo1 x.
An exact proof term for the current goal is H1 f Hf.
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is Hf.
∎