749074bf849727439f584139415f6a985a8aa875Christian Maederclass Eq

32a2f5f00ff72c095b39629101043db4407974f9Christian Maederclass Ord < Eq

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maedertype a : Ord

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maederop f : forall e : Ord . e -> e

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maederop c : a

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder. f (f c) = c;

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maedertype t : Eq

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maederop b : t

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederclasses

6f031207ab25d41ae4740a4151d5946faff4768bChristian MaederEq < Type;

6f031207ab25d41ae4740a4151d5946faff4768bChristian MaederOrd < Type

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maederclass

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederOrd < Eq

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedertypes

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedera : Ord;

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedert : Eq

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maederop b : t

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maederop c : a

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maederop f : forall e : Ord . e -> e

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder. f (f c) = c

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maeder16.3-16.5: ### Hint:

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

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maeder known kinds are: {Eq}

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maeder16.3-16.9: ### Hint:

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maederuntypeable term (with type: ? _v5_a * ? _v5_a) '(f b, b)'

3aa7e4492a7e28b37d1a0b23f5bfe2109f87d4d6Christian Maeder16.7: *** Error: no typing for 'f b = b'