This is an old discussion. Single binding on "or" is a non-orthogonal special case on the language syntax that was introduced in the early days when we only had "infix" CEs. When we started to support prefix CE, the special case was not updated, and as a result, the single binding works only with infix.

The example I've posted is practically identical to Example 7.55, or with binding. So, if it's not in the language, it'd better not be in the documentation :-)

As for the individual binding, as in
(or $t : Trigger(fa == 1)
$t : Trigger(fa == 2))
the documentation ought to caution against using different names, at least when these names are used on the RHS.

I agree that or groups with bindings on patterns are tricky. But is the form that's now accepted by the compiler less error-prone than the one the compiler refuses?