Apply Pex to the current goal.
Let f be given.
Assume Hf: P f.
We prove the intermediate
claim L1:
f = Descr_iii.
Apply func_ext set (set → set) to the current goal.
Let x be given.
Apply func_ext set set to the current goal.
Let y be given.
We will
prove f x y = Eps_i (λz ⇒ ∀h : set → set → set, P h → h x y = z).
We prove the intermediate
claim L2:
∀h : set → set → set, P h → h x y = f x y.
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 → set, P h → h x y = Descr_iii x y.
An
exact proof term for the current goal is
Eps_i_ax (λz ⇒ ∀h : set → set → set, P h → h x y = z) (f x y) 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.
∎