Multiple variables for custom binders should be allowed

[cstolze]

Custom binders do not allow for multiple variables at once:

constant symbol U : TYPE;

constant symbol ∀ : (U → U) → U;
notation ∀ quantifier;

symbol foo ≔ ∀ (λ x, ∀ (λ y, x));
symbol bar ≔ `∀ x, `∀ y, x;

symbol baz ≔ `∀ x y, x; // does not work: [?1.[x] → ?0] and [U] are not unifiable.

As a comparison, custom binders in Coq do support multiple variables:

Axiom U : Type.
Axiom frl : (U -> U) -> U.

Notation "`frl x .. y , p" := (frl (fun x => .. (frl (fun y => p)) ..)) (at level 200, x binder, y binder).

Check (`frl x y z t, x). (* works *)