[Agda] unification using more complex with abstractions

[rick]

I am able to use simple with and rewrite expressions like the following:

data List (X : Set) : Set where
  [] : List X
  _,-_ : (x : X)(xs : List X) -> List X

mapList : {X Y : Set} -> (X -> Y) -> List X -> List Y
mapList f [] = []
mapList f (x ,- xs) = f x ,- mapList f xs

id : {X : Set} -> X -> X
id x = x

data _==_ {X : Set} : X -> X -> Set where
  refl : (x : X) -> x == x

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

mapid : ∀ {X : Set} {x : X} -> (id x == x)
   -> (xs : List X) -> mapList id xs == xs
mapid p [] = refl []
mapid p (x ,- xs) with mapList id xs | mapid p xs
mapid (refl x₁) (x ,- xs) | .xs | refl .xs = refl (x ,- xs)

I proved the same result using rewrite.

Now I am building intuition around more complex with abstractions. For 
example I am trying to prove the following :

[_] : {X : Set} -> X -> List X
[ x ] = x ,- []

wrap : ∀{A} -> List A -> List (List A)
wrap [] = [ [] ]
wrap (x ,- xs) = [ x ,- xs ]

mapid' : ∀ {X : Set} {x : X} -> (id x == x)
   -> (xs : List X) -> wrap (mapList id xs) == wrap xs
mapid' p [] = refl [ [] ]
mapid' p (xs ,- xss) with wrap (mapList id xss) | mapid' p xss
mapid' (refl x) (xs ,- xss) | .(wrap xss) | refl .(wrap xss) = {! ((xs 
,- mapList (λ x₁ → x₁) xss) ,- []) == ((xs ,- xss) ,- []) !}

I have only added a layer around the previous reflexive proof using 
wrap. However, the goal no longer unifies the more complex expression 
listed in the goal.

How do I proceed with these more complex expressions?

-- 
rick