In particular:
for-all bindings are parallel, which is a frequent source of surprise; I think the sequential bindings like gen/let has could be better, and I think the inspiring mathematical notation is also sequential
for-all allows multiple expressions in the body, but all but the last are only executed for side effects; I think the name suggests that only one body expression should be allowed, and this would be less confusing (e.g., ).