424N/Aop __<=__ : Pred (a * a)
424N/Aclasses BoundedOrd < Ord
424N/Avars a: Ord; b: BoundedOrd
424N/Aop __<=__ : Pred (a * a);
424N/A. x <= y /\ y <= z => x <= z
424N/A. x <= y /\ y <= x => x = y
424N/Atype instances a * b: Ord
424N/A. (x, v) <= (y, w) <=> x <= y /\ v <= w
424N/Aclass instance DiscreteOrd < Ord
424N/Avars a: DiscreteOrd; x, y: a
493N/Aop __<=__ : Pred ((a ->? b) * (a ->? b))
424N/Atype instance a ->? b: Ord
424N/A. x <= y <=> def x() => x() <= y()