[Agda] How can I prove associativity of vectors?

[Kenichi Asai]

I think this is FAQ, but I could not find the answer.  How can I prove
associativity of vectors?  If I write:

assoc : forall {a l m n} {A : Set a} ->
        (l1 : Vec A l) -> (l2 : Vec A m) -> (l3 : Vec A n) ->
        (l1 ++ l2) ++ l3 == l1 ++ (l2 ++ l3)
assoc l1 l2 l3 = ?

even the type doesn't type check, because left-hand side has a type
Vec A ((l + m) + n) while right-hand side Vec A (l + (m + n)).
It appears I need a way to identify these two types.  Could somebody
help?

Thank you in advance.

Sincerely,

-- 
Kenichi Asai
-------------- next part --------------
module Append where

open import Data.Nat
open import Data.Vec hiding (_++_)
open import Relation.Binary.PropositionalEquality

_++_ : ? {a m n} {A : Set a} ? Vec A m ? Vec A n ? Vec A (m + n)
[]       ++ ys = ys
(x ? xs) ++ ys = x ? (xs ++ ys)

assoc : ? {a l m n} {A : Set a} ? (l1 : Vec A l) ? (l2 : Vec A m) ? (l3 : Vec A n) ? 
        (l1 ++ l2) ++ l3 ? l1 ++ (l2 ++ l3)
assoc l1 l2 l3 = ?