[Om] Variables not bound in head of binding

[Lars Hellström]

What is the status of / authority for the principle that an OMBIND does not 
cause the variables to become bound in its first child? I thought it was 
explicit in the standard, but now that I look for it, then the closest match 
I find is the following two passages on page 12 of the standard:

   ... The first OpenMath object is the “binder” object. Arguments 2 to n−1 
are always variables to be bound in the “body” which is the nth argument 
object. ...

   ... Suppose an object Ω contains an occurrence of the object 
binding(B,v,C). This object binding(B,v,C) can be replaced in Ω by 
binding(B,z,C′) where z is a variable not occurring free[*] in C and C′ is 
obtained from C by replacing each free (i.e., not bound by any intermediate 
binding construct) occurrence of v by z. This operation preserves the 
semantics of the object Ω. ...

It sort-of follows from this, but rather indirectly. On the other hand I see 
in Davenport & Kohlhase (Unifying Math Ontologies: A tale of two standards, 
2009, p. 12) the passage

   ... the OpenMath2 dictum that the binding operator is not subject
to α-conversion by its own variables ...

which makes me trust my memory of the issue. Still, I don't quite see this 
"dictum" spelt out in the standard. So where would one have picked it up?

Lars Hellström

[*] Actually, now that I reread this sentence, it occurs to me that it is 
slightly wrong. It's not sufficient that z does not occur /free/, since some 
v might occur free in a context where z is bound. Ah, the quagmire of 
variable binding... :-)