[Agda] Confusion about rewrite mechanism

[VinaLx]

Hi everyone!
 
I'm new to agda and was trying to prove some property related to Data.List.partition like this
 partition-++ : ∀ {ℓ} {A : Set ℓ} {xs l r} {p} {P : A → Set p} {p : Decidable P} →                (l , r) ≡ partition p xs → SomeProperty A xs (l ++ r)  
And I pattern-match on xs, and encountered the problem in the [] case, I try to use rewrite and Data.Product.,-injective as follow:
 partition-++ {xs = []} p rewrite ,-injectiveˡ p | ,-injectiveʳ p = ? -- no  
but Agda complained about .l != [] as ,-injectiveʳ required.
 
And I somehow figured out a way out of it:
 partition-++ {xs = []} p with ,-injectiveˡ p ... | l≡[] rewrite l≡[] | ,-injectiveʳ p = ?  
In this case Agda managed to replace .l with [] and ,-injectiveʳ p type checked.
 
And my question is:
  
What's the difference between the first rewrite and the second, why the second rewriting can apply to .l inside of p while the first can't ? What role does with play here?
 
In this scenario what's the correct solution to this? I don't feel right about mine.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180329/2b11e98a/attachment.html>