An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) x HxX (andI (order_rel X a x) (order_rel X x b) Hax Hxb)).