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 HCAUB: C ∩ (A ∪ B) = Empty.
An exact proof term for the current goal is (ex32_8b_C_disjoint_A_union_B X A B S Ts WF C pick HSdef HWFdef HCdef Hpick).
We prove the intermediate claim HBub: B ⊆ (A ∪ B).
An exact proof term for the current goal is (binunion_Subq_2 A B).
We prove the intermediate claim Hsub: (C ∩ B) ⊆ Empty.
Let c be given.
Assume Hc: c ∈ (C ∩ 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 B c Hc).
We prove the intermediate claim HcB: c ∈ B.
An exact proof term for the current goal is (binintersectE2 C B c Hc).
We prove the intermediate claim HcAB: c ∈ (A ∪ B).
An exact proof term for the current goal is (HBub c HcB).
We prove the intermediate claim HcCAUB: c ∈ (C ∩ (A ∪ B)).
An exact proof term for the current goal is (binintersectI C (A ∪ B) c HcC HcAB).
We prove the intermediate claim HcE: c ∈ Empty.
rewrite the current goal using HCAUB (from right to left).
An exact proof term for the current goal is HcCAUB.
An exact proof term for the current goal is HcE.
An exact proof term for the current goal is (Empty_Subq_eq (C ∩ B) Hsub).
∎