Require Export Relations.Relations
               Program.Basics.

Require Export Base.Base.

Require Export Autosubst.Autosubst.

Global Set Implicit Arguments.
Global Unset Strict Implicit.

(* Function composition *)
Notation " x °° y " := (compose x y) (at level 69, right associativity).

(* Make type argument implicit *)
Arguments reflexive [A] R.
Arguments symmetric [A] R.
Arguments transitive [A] R.
Arguments antisymmetric [A] R.
Arguments transp [A] R x y.

(* Notation as used in Paco Library (http://plv.mpi-sws.org/paco/)
     Relation inclusion:             "<2="
     Binary relation union operator: "\2/" *)

Notation "p <2= q" := (forall x0 x1 (PR : p x0 x1 : Prop), q x0 x1 : Prop) (at level 50, no associativity).
Notation "p \2/ q" := (fun x0 x1 => p x0 x1 \/ q x0 x1) (at level 50, no associativity).

(* Empty and unversal relations *)
Notation bot2 := (fun _ _ => False).
Notation top2 := (fun _ _ => True).