Definition Rel (A B : Type) := A -> B -> Prop.
Definition rel (A : Type) := Rel A A.
(* Definition rel [A:Type] := A -> A -> Prop. *)
Definition bin (A : Type) := A -> A -> A.
Definition op (A : Type) := A -> A.
Definition pred (A : Type) := A -> Prop.

Definition ref_rel (A : Type) (r : rel A) := forall x : A, r x x.
Definition sym_rel (A : Type) (r : rel A) := forall x y : A, r x y -> r y x.
Definition trans_rel (A : Type) (r : rel A) :=
  forall x y z : A, r x y -> r y z -> r x z.

Definition bool_rel (A : Type) := A -> A -> bool.