IMO, using cardinality constraints to ensure unicity of events at each step is risky in general, even if safe for particular cases (using signatures is also risky as, depending on how they’re used, it sometimes imposes further implicit cardinality constraints). The worst risk is losing some behaviors (traces).
I think it is safer to follow Lamport’s approach where the unicity of (the observable effect of) actions is a theorem (assert) rather than an axiom (fact). The way to get this in Alloy is to rely on preds for actions, with adequate frame conditions (which will usually induce the said unicity). If you need signatures for visualization of events, this is doable with preds as here.