Let us further introduce a generally useful construct for binding a variable to some (initial) value(s) at one or more of its occurrences in arbitrary formulas. If this is a type-like value, e.g. a non-ground structure or a domain or an exclusion, it can become specialized by subsequent unification.

Occurrence bindings are written as binary `bnd` structures built from a
variable, , and a term, :

In general, `bnd` structures can be used as terms.

Taking a non-ground-structure example,

bindsbnd[X,f[A,B,3,4,5]] is f[1,B,3,D,E]

An analogous finite-domain example,

bindsbnd[X,dom[1,2,3]] is dom[2,3,4,5]

A complementary finite-exclusion example,

bindsbnd[X,exc[1,2,3]] is dom[2,3,4,5]

If the unification partner of an occurrence binding is directly given,
here as the `is`-rhs (right-hand side), the `bnd` structure
can always be equivalently replaced by an initializing (`pre-typing') `is` call:

ForX is f[A,B,3,4,5], X is f[1,B,3,D,E] X is dom[1,2,3], X is dom[2,3,4,5] X is exc[1,2,3], X is dom[2,3,4,5]

The binding construct, pairing a variable with a value, can again be assigned to a variable.
Actually, in our implementation it is generated from
`dom`/`exc`-bound variables at the end of reference chains
to keep track of domain/exclusion specializations
(while non-ground structures can be specialized
via direct in-place assignments).