[Agda] " | condition " in report

[Sergei Meshveliani]

On Sun, 2013-12-22 at 21:35 +0100, Andreas Abel wrote:
> The "| condition" refers to the call to a with-function.
> 
> (Continue below.)
> 
> On 19.12.13 7:22 PM, Sergei Meshveliani wrote:
> ...
> > lemma : (k v : ℕ) → (ps : List (ℕ × ℕ)) → let keys = getKeys ps
> >                                               ps'  = insert k v ps
> >                                            in
> >                                            k ∈ keys → getKeys ps' ≡ keys
> >
> > lemma _ _ []               ()
> > lemma k _ ((k' , _) ∷ ps)  (here k=k')  with  k ≟ k'
> > ...                                     | yes _   =  PE.refl
> > ...                                     | no k≉k' =  ⊥-elim (k≉k' k=k')
> >
> > lemma k v ((k' , v') ∷ ps) (there k∈ks)  with  k ≟ k'
> > ... |
> >       yes k=k' =  PE.refl
> > ... | no k≢k'  =  goal
> 
> This proof is completed simply by
> 
> ... | no k≢k'  =  PE.cong (_∷_ k') (lemma k v ps k∈ks)
> 
> Merry Christmas,
> Andreas
> 


Thank you. This was silly of me to overlook such a natural proof.

There remains a question:
why the checker does not accept my awkward proof for  goal ?
Is it a bug?

Merry Christmas,

------
Sergei