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

Sergei Meshveliani mechvel at botik.ru
Wed Dec 18 12:23:10 CET 2013

```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

```