GOV-Vote rule irregularities

In the `Vote` step, the `ast` (`GovActionState`) is not determined by any of the inputs:
```agda
GOV-Vote : ∀ {x k ast} → let open GovEnv Γ in
(aid , ast) ∈ setFromList s
→ canVote pparams (action ast) role
────────────────────────────────
(Γ , k) ⊢ s ⇀⦇ inj₁ record { gid = aid ; role = role ; credential = cred ; vote = v ; anchor = x } ,GOV'⦈
addVote s aid role cred v
```
In case the same `aid` appears several time in the state this could be a problem. This should never happen but there is nothing in the types that prevents it.

At first I thought this made the rule non-computational, but looking at the details I'm not sure this is true. The `addVote` function updates all instances of the given `aid`, so even if you pick different ones you get the same state.

It's still a bit fishy since you could have two occurrences of `aid` one where you `canVote` and one where you can't, and we'll update both in the rule.

A simple thing we could do is add a precondition `GOV-Vote` requiring `aid` to be unique. More work (but arguably nicer) would be to change the type of the state to something that guarantees left-uniqueness, keeping in mind that the order of the entries is important.