Let X, A, B, S, Ts, WF, C and pick be given.
Assume HSdef: S = X ∖ (A ∪ B).
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.
We prove the intermediate claim HCsubS: C ⊆ S.
An exact proof term for the current goal is (ex32_8b_C_subset_S X A B S Ts WF C pick HWFdef HCdef Hpick).
Apply Empty_Subq_eq to the current goal.
Let c be given.
Assume Hc: c ∈ C ∩ (A ∪ B).
We will prove c ∈ Empty.
We prove the intermediate claim HcC: c ∈ C.
An exact proof term for the current goal is (binintersectE1 C (A ∪ B) c Hc).
We prove the intermediate claim HcAB: c ∈ (A ∪ B).
An exact proof term for the current goal is (binintersectE2 C (A ∪ B) c Hc).
We prove the intermediate claim HcS: c ∈ S.
An exact proof term for the current goal is (HCsubS c HcC).
We prove the intermediate claim HcXminus: c ∈ (X ∖ (A ∪ B)).
rewrite the current goal using HSdef (from right to left).
An exact proof term for the current goal is HcS.
We prove the intermediate claim HcNotAB: ¬ (c ∈ (A ∪ B)).
An exact proof term for the current goal is (setminusE2 X (A ∪ B) c HcXminus).
An exact proof term for the current goal is (HcNotAB HcAB (c ∈ Empty)).
∎