Let X, A, B, S, Ts, WF, C and pick be given.

Assume HWFdef: WF = {W0 ∈ 𝒫 S|ex32_8_WFpred X A B S Ts W0}.

Assume HCdef: C = {pick W0|W0 ∈ WF}.

Assume Hpick: ∀W : set, W ∈ WF → pick W ∈ W.

rewrite the current goal using HCdef (from left to right).

Let c be given.

Assume Hc: c ∈ {pick W0|W0 ∈ WF}.

Apply (ReplE_impred WF (λW0 : set ⇒ pick W0) c Hc) to the current goal.

Let W0 be given.

Assume HW0: W0 ∈ WF.

Assume HcEq: c = pick W0.

We prove the intermediate claim HpickW0: pick W0 ∈ W0.

An exact proof term for the current goal is (Hpick W0 HW0).

We prove the intermediate claim HW0': W0 ∈ {W1 ∈ 𝒫 S|ex32_8_WFpred X A B S Ts W1}.

rewrite the current goal using HWFdef (from right to left).

An exact proof term for the current goal is HW0.

We prove the intermediate claim HW0Pow: W0 ∈ 𝒫 S.

An exact proof term for the current goal is (SepE1 (𝒫 S) (λW1 : set ⇒ ex32_8_WFpred X A B S Ts W1) W0 HW0').

We prove the intermediate claim HW0subS: W0 ⊆ S.

An exact proof term for the current goal is (PowerE S W0 HW0Pow).

rewrite the current goal using HcEq (from left to right).

An exact proof term for the current goal is (HW0subS (pick W0) HpickW0).

∎