Let a and b be given.

Assume Hab.

We prove the intermediate claim HaR: a ∈ R.

An exact proof term for the current goal is (RltE_left a b Hab).

We prove the intermediate claim Hb: ¬ (Rlt a a) ∧ Rlt a b.

Apply andI to the current goal.

An exact proof term for the current goal is (not_Rlt_refl a HaR).

An exact proof term for the current goal is Hab.

An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ¬ (Rlt x0 a) ∧ Rlt x0 b) a HaR Hb).

∎