[Agda] x \in (gfilter _ ys)

[Sergei Meshveliani]

People,                                                                                 
I have the next round in my battle with a filtered list proofs.
I need to proof that 
                     x ∈  gfilter (toMaybe' P?) ys 
if                   x ∈  ys              
                     and  P Respects _≈_,  and (P x).

This needs to be by the function  in-gfiltered-id  below:

-----------------------------------------------------------------
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.Unary   using (Decidable)
open import Relation.Binary  using (Rel; Setoid; module Setoid;
                                    DecSetoid; module DecSetoid)
open import Relation.Binary.Core using (_Respects_; IsEquivalence;
                                        module IsEquivalence)
open import Data.Empty    using (⊥-elim)
open import Data.Maybe    using (Maybe; just; nothing)
open import Data.Product  using (_×_; _,_)
open import Data.List     using (List; []; _∷_; map; gfilter)
open import Data.List.Any using (Any; module Any; module Membership)

       
toMaybe' : ∀ {p} {C : Set} {P : C → Set p} → Decidable P → C → Maybe C
toMaybe' P? x  with P? x
...                     | yes _ =  just x
...                     | _     =  nothing


postulate anything : ∀ {a} {A : Set a} → A       -- for debug  

in-gfiltered-id : ∀ {l p} (A : Setoid 0L l) →    -- case f = id  
  let
     open Setoid A using (_≈_) renaming (Carrier to C)
     _∈_ = Membership._∈_ A
  in
  (P : C → Set p) → (P? : Decidable P) → P Respects _≈_ → (x : C) → 
  P x → (ys : List C) → x ∈ ys →
                        x ∈ (gfilter (toMaybe' P?) ys)

open Any

in-gfiltered-id {l} {p} A P P? pCong x Px (y ∷ ys) (here x=y) =

  (let triple : Dec (P y) × Maybe C × List C
       triple = (P? y , toMb y , filterMb (y ∷ ys))
   in
   case triple of \
   { (no ¬Py , _ ,      _  ) → let Py = pCong x=y Px in  ⊥-elim (¬Py Py)
   ; (yes Py , just y , z ∷ zs) →
               let 
                  y=z : y ≈ z
                  y=z = _ -- ? refl                          
                  x=z : x ≈ z
                  x=z = anything -- ? trans x=y y=z

                  p : Any {0L} {_} (_≈_ x) (z ∷ zs)
                  p = here x=z                      -- ?
                  -- here {0L} {_} {C} (_≈_ x) (z ∷ zs) {z} {zs} x=z    
                  -- here {A = C} (_≈_ x) (z ∷ zs) {z} {zs} x=z  
               in p

   ; (yes Py , just y ,  []) → _  -- ?
   ; (yes Py , nothing , _ ) → _  -- ?
   }
  )
  where
  open Setoid A using (_≈_) renaming (Carrier to C)
  open IsEquivalence (Setoid.isEquivalence A) using (refl; sym; trans)
  toMb     = toMaybe' P?
  filterMb = gfilter toMb

in-gfiltered-id A P P? pCong x Px (y ∷ ys) (there x∈ys) = _

            -- after failing with `here', I have not hope with `there'

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

1. How to prove  in-gfiltered-id ?

2. A note:  instead of  let triple : ...
                            triple = ( ... )
                        in   
                        case triple of ...

above it is natural to write
      
            case (P? y , toMb y , filterMb (y ∷ ys)) of ...,

but this latter is not type-checked (in Agda-2.3.2.1).

3. The report is 
-------------
Cannot instantiate the metavariable _84 to solution 
Any (_≈_ x) (z ∷ zs) since it contains the variable z which is not in
scope of the metavariable or irrelevant in the metavariable but relevant
in the solution when checking that the expression p has type
_B_84 A P P? pCong x Px y ys x=y
-------------

What is wrong with  z  ? 

4. I tried to write  `here' in full:
                        
           p = here {0L} {_} {C} (_≈_ x) (z ∷ zs) {z} {zs} x=z
 
And it reports
-------------------
Any (_P_100 A P P? pCong x Px y ys x=y Py y z zs)
(_x_101 A P P? pCong x Px y ys x=y Py y z zs ∷
 _xs_102 A P P? pCong x Px y ys x=y Py y z zs)
should be a function type, but it isn't
when checking that 
                          (z ∷ zs) {z} {zs} x=z 

are valid arguments to a function of type
Any (_P_100 A P P? pCong x Px y ys x=y Py y z zs)
(_x_101 A P P? pCong x Px y ys x=y Py y z zs ∷
 _xs_102 A P P? pCong x Px y ys x=y Py y z zs)
---------------------
   
Thank you in advance for explanation,

------
Sergei