<p>Hi everyone!</p>

<p>I'm new to agda and was trying to prove some property related to <code>Data.List.partition</code> like this</p>

<pre><code>partition-++ : ∀ {ℓ} {A : Set ℓ} {xs l r} {p} {P : A → Set p} {p : Decidable P} →
               (l , r) ≡ partition p xs → SomeProperty A xs (l ++ r)
</code></pre>

<p>And I pattern-match on <code>xs</code>, and encountered the problem in the <code>[]</code> case, I try to use <code>rewrite</code> and <code>Data.Product.,-injective</code> as follow:</p>

<pre><code>partition-++ {xs = []} p rewrite ,-injectiveˡ p | ,-injectiveʳ p = ? -- no
</code></pre>

<p>but Agda complained about <code>.l != []</code> as <code>,-injectiveʳ</code> required.</p>

<p>And I somehow figured out a way out of it:</p>

<pre><code>partition-++ {xs = []} p with ,-injectiveˡ p
... | l≡[] rewrite l≡[] | ,-injectiveʳ p = ?
</code></pre>

<p>In this case Agda managed to replace <code>.l</code> with <code>[]</code> and <code>,-injectiveʳ p</code> type checked.</p>

<p>And my question is:</p>

<ol>
<li>What's the difference between the first <code>rewrite</code> and the second, why the second rewriting can apply to <code>.l</code> inside of <code>p</code> while the first can't ? What role does <code>with</code> play here?</li>

<li>In this scenario what's the correct solution to this? I don't feel right about mine.</li>
</ol>