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