2N/Aclass Eq
2N/Aclass Ord < Eq
2N/A
2N/Atype a : Ord
2N/A
2N/Aop f : forall e : Ord . e -> e
2N/A
2N/Aop c : a
2N/A
2N/A. f (f c) = c
2N/A
2N/Atype t : Eq
2N/A
2N/Aop b : t
2N/A
2N/A. f b = b
2N/A