Apply Pex to the current goal.
Let f be given.
Assume Hf: P f.
We prove the intermediate
claim L1:
f = Descr_ii.
Apply func_ext set set to the current goal.
Let x be given.
We will
prove f x = Eps_i (λy ⇒ ∀h : set → set, P h → h x = y).
We prove the intermediate
claim L2:
∀h : set → set, P h → h x = f x.
Let h be given.
Assume Hh.
rewrite the current goal using Puniq f h Hf Hh (from left to right).
An exact proof term for the current goal is (λq H ⇒ H).
We prove the intermediate
claim L3:
∀h : set → set, P h → h x = Descr_ii x.
An
exact proof term for the current goal is
Eps_i_ax (λy ⇒ ∀h : set → set, P h → h x = y) (f x) L2.
An exact proof term for the current goal is L3 f Hf.
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is Hf.
∎