(* RelationClasses, actually defined in Relation_Definitions *)
Definition relation (A : Type) := A -> A -> Prop.

(* CRelationClasses *)
Definition crelation (A : Type) := A -> A -> Type.