Hi Kenichi, see https://lists.chalmers.se/pipermail/agda/2016/009069.html for how associativity of vectors (and `vs ++ [] == vs` as well) can be proven without the need for `subst` or `rewrite`.