[Agda] How can I prove associativity of vectors?

[Helmut Grohne]

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

You have a number of options here:

 * Use Relation.Binary.HeterogeneousEquality rather than
   PropositionalEquality.
 * Use Data.Vec.Equality rather than PropositionalEquality.
 * Use Relation.Binary.PropositionalEquality.Core.subst and
   Data.Nat.Properties.Simple.+-assoc to make the types match.

The last option gets ugly but allows you to keep using
PropositionalEquality.

Helmut