Let b be given.
Assume Hb: b ∈ S_Omega.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ {x0 ∈ S_Omega|order_rel S_Omega x0 b}.
We prove the intermediate claim HxS: x ∈ S_Omega.
An exact proof term for the current goal is (SepE1 S_Omega (λx0 : set ⇒ order_rel S_Omega x0 b) x Hx).
We prove the intermediate claim Hrel: order_rel S_Omega x b.
An exact proof term for the current goal is (SepE2 S_Omega (λx0 : set ⇒ order_rel S_Omega x0 b) x Hx).
We prove the intermediate claim Hmem: x ∈ b.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem S_Omega x b S_Omega_well_ordered_set Hrel).
We prove the intermediate claim HrelInh: order_rel Sbar_Omega x b.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered Sbar_Omega x b Sbar_Omega_well_ordered_set Hmem).
Apply (SepI S_Omega (λx0 : set ⇒ order_rel Sbar_Omega x0 b) x HxS) to the current goal.
An exact proof term for the current goal is HrelInh.
Let x be given.
Assume Hx: x ∈ {x0 ∈ S_Omega|order_rel Sbar_Omega x0 b}.
We prove the intermediate claim HxS: x ∈ S_Omega.
An exact proof term for the current goal is (SepE1 S_Omega (λx0 : set ⇒ order_rel Sbar_Omega x0 b) x Hx).
We prove the intermediate claim Hrel: order_rel Sbar_Omega x b.
An exact proof term for the current goal is (SepE2 S_Omega (λx0 : set ⇒ order_rel Sbar_Omega x0 b) x Hx).
We prove the intermediate claim Hmem: x ∈ b.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem Sbar_Omega x b Sbar_Omega_well_ordered_set Hrel).
We prove the intermediate claim HrelSo: order_rel S_Omega x b.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered S_Omega x b S_Omega_well_ordered_set Hmem).
Apply (SepI S_Omega (λx0 : set ⇒ order_rel S_Omega x0 b) x HxS) to the current goal.
An exact proof term for the current goal is HrelSo.
∎