[Agda] cancel-just-in≡

[Sergei Meshveliani]

People,
I am trying to prove the congruence of  Data.List.gfilter  by  _≗_ 
and  _≡_.

By the second argument  xs : List A,  it is proved simply by   
PE.cong (gfilter p)
   where
   open import Relation.Binary.PropositionalEquality as PE 
                                                     using (_≡_; _≗_)

For the first argument, I have  
              xs : List A,   p p' : A -> Maybe B,  p≗p' : p ≗ p',

and need to prove   gfilter p xs ≡ gfilter p' xs.

PE.cong (\ p -> gfilter p xs) p≗p' PE.refl

does not work here (need it?).

Then, I try recursion by the list construction:   

  cong₁-gfilter (x ∷ xs) {p} {p'} p≗p' =  eq
    where
    ...

And then, need to prove   just x ≡ just y → x ≡ y.  

I suspect that a dotted pattern must help, but fail.
I write for testing:

 cancel-just-in≡ : {A : Set} {x y : A} → let _≡A_ = _≡_ {A = A}
                                             _≡m_ = _≡_ {A = Maybe A}
                                         in
                                         just x ≡m just y → x ≡A y

 cancel-just-in≡ {A} {x} {y} jx=jy  with  just x | just y
                                       	       	
 ... | just x | .(just x) =  PE.refl

The  development Agda of November 2013 (MAlonzo)  
reports  

Repeated variables in left hand side: x
when scope checking the left-hand side
cancel-just-in≡ {A} {x} {y} jx=jy in the definition of
cancel-just-in≡

1) I do not see here any LHS variable repetition, because second  x  is
after `with'.
2) How to prove  cancel-just-in≡ ?
3) How to prove  cong₁-gfilter ?

Thank you in advance for explanation,

------
Sergei