Improve error messages for operators

[fizruk]

@TashiWalde reports that ≥ is not supported, but also that the error message is confusing.

Example code:

#def min
-- works
  ( A : U)
  ( σ : 2 → A)
  : (2 × 2) → A
  := \ (t , s) → recOR ( t ≤ s ↦ σ t , s ≤ t ↦ σ s)

#def min'
-- doesn't work
  ( A : U)
  ( σ : 2 → A)
  : (2 × 2) → A
  := \ (t , s) → recOR ( t ≤ s ↦ σ t , t ≥ s ↦ σ s)

Current error message:

when inferring type for term
  t ≥

when unifying expected type
  U
with actual type
  CUBE
for term
  2

This is because ≥ is treated as a regular variable name (since it is not reserved like ≤).