[Agda] elem x (filter xs)

[Sergei Meshveliani]

Can you, please, help with the following example with a filtered list?

-----------------------------------------------------------------------
open import Level            using (Level) renaming (zero to 0L)
open import Function         using (case_of_)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.Core using (_≡_; refl)
open import Data.Empty       using (⊥-elim)
open import Data.Nat         using (ℕ; _≟_)
open import Data.List        using (List; []; _∷_)
open import Data.List.Any    using (Any; module Any)

postulate member  : ℕ → Set 
postulate member? : (x : ℕ) → Dec (member x) 

filterMem : List ℕ → List ℕ
filterMem []       = []
filterMem (x ∷ xs)  with member? x
...                    | yes _ = x ∷ (filterMem xs)
...                    | _     = filterMem xs

open Any

lemma1 : (x : ℕ) → member x → Any (_≡_ x) (filterMem (x ∷ []))

lemma1 x mem-x  with  member? x | filterMem (x ∷ [])

...                 | (yes _) | .(x ∷ []) =  here {x} {[]} refl 

-----------------------------------------------------------------------

This is an attempt to prove this trivial statement:

  if  x  is in a subset  S  then  x  is in  filterMem (x :: []),
  where  filterMem  filters my membership to S. 

To be more explicit, I replace  x \in ys  with  Any (_≡_ x) ys. 

The  Agda-2.3.2.1  (lib-0.7)  report is
------
Failed to infer the value of dotted pattern
when checking that the pattern .(x ∷ []) has type List ℕ
------

1. Having  mem-x : member x,  why does not it accept  .(x ∷ [])
   for  filterMem (x ∷ [])  ?

2. Then, I change the last line to 

...           | (yes _) | (_ ∷ _) =  here {x} {[]} refl 

And it reports 
-------
ℕ !=< Level of type Set
when checking that the expression x has type Level
-------

This is on the {x} occurrence in the last line.
Why  x  needs to be of  Level ?
`here' has not Level among its argument types.

3. Having  mem-x  and normalization by  filterMem,
   I expected that a simple                  `` = here refl''  
would do the implementation. But it does not.

4. Changing to 
...     | (yes _) | y :: ys =  here {x} {_} x=y
                               where
                               x=y = x ≡ y
                               x=y = ?

we need to prove x ≡ y,  which is not simpler than the initial goal.


5. How to prove the goal?


Thank you in advance for explanation,

------
Sergei