286N/Aclass Eq

286N/Aclass Ord < Eq

286N/Atype a : Ord

286N/Aop f : forall e : Ord . e -> e

286N/Aop c : a

286N/A. f (f c) = c;

286N/Atype t : Eq

286N/Aop b : t

286N/Aclasses

286N/AEq < Type;

286N/AOrd < Type

286N/Aclass

286N/AOrd < Eq

286N/Atypes

286N/Aa : Ord;

286N/At : Eq

286N/Aop b : t

286N/Aop c : a

286N/Aop f : forall e : Ord . e -> e

286N/A. f (f c) = c

286N/A### Hint 16.3-16.5,

286N/Aconstrain 't : Ord' is unprovable of '(op f : forall e : Ord . e -> e) (op b : t)'

286N/A known kinds are: {Eq}

286N/A### Hint 16.3-16.9,

286N/Auntypeable term (with type: ? _v5_a * ? _v5_a) '(f b, b)'

286N/A*** Error 16.7, no typing for 'f b = b'

286N/A