class Eq
class Ord < Eq
type a : Ord
op f : forall e : Ord . e -> e
op c : a
. f (f c) = c
type t : Eq
op b : t
. f b = b