Fail Notation "'forall' x  ..  y ',' P " := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder).