Let a, b and x be given.

Assume Hx: x ∈ open_interval a b.

We prove the intermediate claim Hprop: Rlt a x ∧ Rlt x b.

An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ Rlt a x0 ∧ Rlt x0 b) x Hx).

An exact proof term for the current goal is (RltE_right x b (andER (Rlt a x) (Rlt x b) Hprop)).

∎