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;

classes

Eq : Type;

Ord : Type

class

Ord < Eq

types

a : Ord;

t : Eq

op b : t %(op)%

op c : a %(op)%

op f : forall e : Ord . e -> e %(op)%

. f (f c) = c

. f b = b

### Hint 16.3,

constrain 't : Ord' is unprovable

known kinds are: {Eq}

*** Error 16.3,

in term '(op f : forall e : Ord . e -> e) (op b : t) = (op b : t)' of type 'Unit'

unresolved constraints

'{t : Ord}'