[Agda] Associativity and Heterogeneous Equality

[effectfully]

Conor McBride gave clear explanations in the thread Kenichi Asai mentioned:

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

Applying the technique to this case:

    postulate
      assoc-++ : ∀ {α} {A : Set α} (xs {ys zs} : List A) -> xs ++ ys
++ zs ≅ (xs ++ ys) ++ zs

    assoc-+++ : ∀ {xs ys zs} (a : HList xs) (b : HList ys) (c : HList
zs) -> a +++ b +++ c ≅ (a +++ b) +++ c
    assoc-+++ [] b c = refl
    assoc-+++ {_ ∷ xs} {ys} {zs} (x ∷ a) b c =
      cong₂ (λ xs (hxs : HList xs) → x HList.∷ hxs) (assoc-++ xs)
(assoc-+++ a b c)

There are other ways to write the same definition: using `with' like
in Conor McBride's answer or using indexed `cong' like in

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

However `with' seems less clean and more verbose to me, and I advise
to not use indexed `cong's, `subst's and other similar functions (I
used them previously, and it made my code totally unreadable; you can
check some definitions in [1]). The usual `cong's are straight and
explicit, so it's a good choice.

[1] https://github.com/effectfully/Ouroboros/blob/master/Prelude.agda