include "logic/pts.ma".

ninductive Compare: Type[0] ≝
  Equal: Compare
| Less: Compare
| Greater: Compare.