[Agda] strange PE.refl ambiguity

[Sergei Meshveliani]

People,
I have

  open import Relation.Binary.PropositionalEquality as PE using (_≡_)
  ...
  
  addMany : List C×ℕ → Multiset → Multiset
  addMany ps mS =  foldr add1 mS ps

  ...

  cong₂addMany : {ps : List C×ℕ} → (addMany ps) Preserves _=ms_ ⟶ _=ms_

  cong₂addMany {[]}     {_}  {_}   mS=ms=mS' =  mS=ms=mS'
  cong₂addMany {p ∷ ps} {mS} {mS'} mS=ms=mS' =
    begin-ms
      addMany (p ∷ ps) mS      =ms[ =ms-reflexive (lemma mS) ]

                            -- =ms[ =ms-reflexive PE.refl]

      add1 p (addMany ps mS)   =ms[ cong₂add1 {p} $ cong₂addMany {ps}
                                                    {mS} {mS'} mS=ms=mS'
                                  ]
      add1 p (addMany ps mS')  =ms[ =ms-reflexive $ lemma mS' ]
      addMany (p ∷ ps) mS'
    end-ms
    where
    lemma : (s : Multiset) → addMany (p ∷ ps) s ≡ add1 p (addMany ps s)
    lemma _ = PE.refl

Here 'lemma'  is only by normalization by the definition of
Data.List.foldr. 

And I do not understand:  why replacing  (lemma mS)  with  PE.refl
leads to "unsolved metas".
How to avoid writing additional signatures after `where' which actually
express only  PE.refl ?
In earlier examples, it worked merely PE.refl instead of a similar
lemma. And this particular example occurs "unsolved", and adding `lemma'
complicates the code.

Thanks,

------
Sergei