An exact proof term for the current goal is (andER (a ∈ R) (b ∈ R) (andEL (a ∈ R ∧ b ∈ R) (a < b) H)).