Let a and b be given.
Assume Hab.
We prove the intermediate
claim HbR:
b ∈ R.
An
exact proof term for the current goal is
(RltE_right a b Hab).
We prove the intermediate
claim Hprop:
Rlt a b ∧ ¬ (Rlt b b).
Apply andI to the current goal.
An exact proof term for the current goal is Hab.
An
exact proof term for the current goal is
(not_Rlt_refl b HbR).
An
exact proof term for the current goal is
(SepI R (λx0 : set ⇒ Rlt a x0 ∧ ¬ (Rlt b x0)) b HbR Hprop).