# Recursive notations with forall quantifier

How can I implement a notation of the form: ∀ x ≤ y ≤ .. ≤ z ≤ t, φ in Coq?

A similar notation (but without quantifiers) appears here

Notation "x ≤ y  ≤ ..  ≤ z ≤ t" :=
((fun b A a => a <= b /\ A b) y
.. ((fun b A a => a <= b /\ A b) z (fun b => b <= t))
.. x)
(at level 70, y at next level, z at next level, t at next level).


But I was unsuccessful in putting forall quantifiers to it.