[Agda] join 2 `with'|

[mechvel at scico.botik.ru]

People,

Having the proof

   prove : (k∈ks : k ∈ ks) → proj₂ (lookupIf∈ k (p ∷ ps) k∈k':ks) ≡
                             proj₂ (lookupIf∈ k ps k∈ks)
   prove k∈ks  with  k ≟ k'                                           -- 
(I)

   ... | yes k≡k' =  ⊥-elim $ k≉k' k≡k'
   ... | no _     with  lookup k ps
   ...                | inj₁ _    =  PE.refl
   ...                | inj₂ k∉ks =  ⊥-elim $ k∉ks k∈ks


(I do not give the complete code),

I try to rewrite it in a bit simpler way by joining it into one `with' 
clause:


   prove k∈ks  with  k ≟ k' | lookup k ps                              -- 
(II)

   ... | yes k≡k' | _         =  ⊥-elim $ k≉k' k≡k'
   ... | no _     | inj₁ _    =  PE.refl
   ... | no _     | inj₂ k∉ks =  ⊥-elim $ k∉ks k∈ks


(I) is type-checked, and (II) is not.

Is this natural for Agda to decide so?

(I have spent 4 hours trying to prove a similar real and evident 
example. Then tried to split `with' into two, and this has succeeded).

Thanks,

------
Sergei