I think we can do better in this part:
Evaluate BODY with bindings made by matching PATTERN to each
element of LIST in turn. PATTERN is a pcase pattern
I think using "matching" here is detrimental to understanding what's
going on, which is a destructuring binding that uses pcase patterns.
(The "matching" here is between the structures of PATTERN and elements
of LIST, but the usual meaning of "matching" in Emacs is different,
especially when "patterns" are mentioned nearby. So we should not use
"matching" here, at least not without significant qualifiers, like
"structure matching" or somesuch.)
And this:
Should the matching fail for any LIST element, the results are
undefined.
should be reworded to explain that elements of LIST should have a
structure compatible with PATTERN, so that the destructuring works.