[Agda] more unification using more complex with abstractions

[Nils Anders Danielsson]

On 2018-07-31 20:00, rick wrote:
> Can I use the lemma and if so how can I use it to cause Agda to unify
> mu?

{-# BUILTIN EQUALITY _==_ #-}

mu : ∀ {X} (xss : List (List X)) →
      listMap (unit >> mult) xss == xss
mu []           = refl []
mu (xs₁ ,- xs₂) rewrite lem xs₁ | mu xs₂ = refl _

-- 
/NAD