[Agda] How can I prove associativity of vectors?

[Sergei Meshveliani]

On Tue, 2014-12-16 at 23:55 +0900, Kenichi Asai wrote:
> 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?


May be, this can be used instead?

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

Regards,

------
Sergei