Notation "∀ x .. y , P" := (∀ x, .. (∀ y, P) ..)
  (at level 10, x binder, y binder, P at level 200,
  format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope.
Notation "∃ x .. y , P" := (∃ x, .. (∃ y, P) ..)
  (at level 10, x binder, y binder, P at level 200,
  format "'[ ' '[ ' ∃ x .. y ']' , '/' P ']'") : type_scope.

Notation "x ∨ y" := (x ∨ y) (at level 85, right associativity) : type_scope.
Notation "x ∧ y" := (x ∧ y) (at level 80, right associativity) : type_scope.
Notation "x → y" := (x → y)
  (at level 99, y at level 200, right associativity): type_scope.

Notation "x ↔ y" := (x ↔ y) (at level 95, no associativity): type_scope.
Notation "¬ x" := (¬x) (at level 75, right associativity) : type_scope.
Notation "x ≠ y" := (x ≠ y) (at level 70) : type_scope.

Notation "'λ' x .. y , t" := (fun x ⇒ .. (fun y ⇒ t) ..)
  (at level 10, x binder, y binder, t at level 200,
  format "'[ ' '[ ' 'λ' x .. y ']' , '/' t ']'").

Notation "x ≤ y" := (le x y) (at level 70, no associativity).
Notation "x ≥ y" := (ge x y) (at level 70, no associativity).

Notation "∃! x .. y , p" :=
  (ex (unique (λ x, .. (ex (unique (λ y, p))) ..)))
    (at level 200, x binder, right associativity)
  : type_scope.