[Agda] Proof involving associativity of ++ of vectors

[Shin-Cheng Mu]

Hi,

On Oct 16, 2009, at 11:13 PM, Jean-Philippe Bernardy wrote:
>  thm' : ∀ {m n} (xs : Vec A m) → (zs : Vec A n) →
>           P xs → Q (zs ++ xs)
>  thm' [] _ _ = {!...!}
>  thm' {suc m} {n} (x ∷ xs) zs pxs with (n + suc m) | zs ++ x ∷ xs  
> |
> sym (eq1 zs x xs)
>  thm' {suc m} {n} (_∷_  x xs) zs pxs | ._ | ._ | refl  = thm' xs (zs
> ++ [ x ]) (red pxs)

This works well like magic. Thank you!

On Oct 16, 2009, at 11:48 PM, Nils Anders Danielsson wrote:
> I believe that the discussion in the following thread (Congruence and
> substitutivity rules in heterogeneous equality) is relevant:
>
> http://thread.gmane.org/gmane.comp.lang.agda/954

Indeed. I'll look at that thread again. Thanks!

sincerely,
Shin