e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncclass Eq

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncclass Ord < Eq

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsynctype a : Ord

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncop f : forall e : Ord . e -> e

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncop c : a

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsync. f (f c) = c;

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsynctype t : Eq

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncop b : t

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncclasses

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncEq < Type;

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncOrd < Type

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncclass

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncOrd < Eq

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsynctypes

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsynca : Ord;

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsynct : Eq

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncop b : t

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncop c : a

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncop f : forall e : Ord . e -> e

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsync. f (f c) = c

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsync16.3-16.5: ### Hint:

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncconstrain 't : Ord' is unprovable of '(op f : forall e : Ord . e -> e) (op b : t)'

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsync known kinds are: {Eq}

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsync16.3-16.9: ### Hint:

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsyncuntypeable term (with type: ? _v5_a * ? _v5_a) '(f b, b)'

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsync16.7: *** Error: no typing for 'f b = b'

e0e0c19eefceaf5d4ec40f9466b58a771f50e799vboxsync