[Agda] vs++[]==vs for vectors

[Kenichi Asai]

Dear all,

I want to prove that vs ++ [] == vs for a vector vs of length n.
Simply writing this statement results in a type error, because the
left-hand side has type Vec N (n + 0) while the right-hand side
Vec N n.  The problem is similar to the associativity of vector append
that I asked years ago:

https://lists.chalmers.se/pipermail/agda/2014/007282.html

This time, I am trying to prove it using subst found in
Relation.Binary.PropositionalEquality, and formulated the statement as:

subst (Vec N) (+-right-identity n) (vs ++ []) == vs

But I could not prove it.  How can I prove it?  It seems I don't
understand how I can pattern match on (+-right-identity n), so that
subst is unfolded.

Thanks in advance.

Sincerely,

-- 
Kenichi Asai
-------------- next part --------------
module test where

open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Vec
open import Relation.Binary.PropositionalEquality

appN : ? {n} (? : Vec ? n) ? subst (Vec ?) (+-right-identity n) (? ++ []) ? ?
appN [] = refl
appN (_?_ {n} ? ?) = {!!}