[Agda] x ∈ (append y xs) → ..

[Sergei Meshveliani]

Can anybody explain, please, why the below  lemma1  is more difficult to
prove to Agda than  lemma0
?

append0 : List ℕ → List ℕ
append0 []       =  0 ∷ []
append0 (x ∷ xs) =  x ∷ (append0 xs)

append : ℕ → List ℕ → List ℕ
append x []       =  x ∷ []
append x (y ∷ xs) =  y ∷ (append x xs)

open module Mem-ℕ = Membership natSetoid using (_∈_)

---------------------------------------------------------------------        
lemma0 : (x : ℕ) → (xs : List ℕ) → x ∈ (append0 xs) → x ≡ 0 ⊎ (x ∈ xs)

lemma0 _ [] (here x=y) =  inj₁ x=y
...
-- skip other patterns

--------------------------------------------------------------------
lemma1 : (x y : ℕ) → (xs : List ℕ) → x ∈ (append y xs) → 
                                         x ≡ y ⊎ (x ∈ xs)
lemma1 _ _ [] (here x=y) =  inj₁ x=y
--------------------------------------------------------------------

lemma0  is proved in a natural way, and is type-checked.

For  lemma1,  
I expected of the checker to report of "missing patterns" -- which will
mean that the first pattern is all right.

And the   development Agda of November ~20 2013
reports
"
I'm not sure if there should be a case for the constructor here,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  x₁ ∷ xs₁ ≟ append y xs
when checking the definition of lemma1
".

I fix the proof by writing a strange complicated code instead of the
first pattern:

  lemma1 x y [] x∈app-y-xs =  inj₁ x=y    
    where 
    x=y : x ≡ y           
    x=y  with x∈app-y-xs                                            
    ... | here eq = eq                                      
    ... | there ()                                            
    
This looks strange: the checker is sure and "is not sure" in a pattern
which is actually the same.
I guess that for the first pattern, it is not sure that  append y []
is non-empty. But it follows only from normalization.

Does this present a bug?

Thanks,

------
Sergei