# [Agda] cancel-just-in≡

Sergei Meshveliani mechvel at botik.ru
Sat Dec 7 12:01:14 CET 2013

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

```