[Agda] strange " ,′ "

[Sergei Meshveliani]

People,
for the code fragment 

----------------------------------------
   let ys = del _≟_ x xs'

       ⊆to : x ∷ xs ⊆ x ∷ ys
       ⊆to {z} z∈x:xs =
           case
               (x ≟ z , z∈x:xs)
            of \
            { (_ ,       here z=x  ) → here z=x
            ; (yes x=z , _         ) → here $ ≈sym x=z
            ; (no x≉z ,  there z∈xs) →
                               let z∈xs' = proj₁ xs='xs' z∈xs
                                   z∈ys  = ∈del-x-xs-if _≟_ x≉z z∈xs'
                               in  there z∈ys
            }

       ⊆from : x ∷ ys ⊆ x ∷ xs
       ⊆from {z} z∈x:ys =
             case
                 (x ≟ z , z∈x:ys)
             of \
             { (_ ,       here z=x  ) → here z=x
             ; (yes x=z , _         ) → here $ ≈sym x=z
             ; (no x≉z ,  there z∈ys) → let z∈xs' : z ∈ xs'
                                            z∈xs' = del-x-xs⊆xs _≟_ z∈ys
                                            z∈xs = proj₂ xs='xs' z∈xs'
                                        in  there z∈xs
             }
   ...
-----------------------------------------


Agda 2.4.2  reports

  Cannot instantiate the metavariable _1653 to solution x₁ ∷ xs₁
  ...

This is for the line of the first pattern after the second  `of' 
-- not the first one!
And this is fixed by replacing _,_ with _,′_ in the pair after the
second  'case'.

This all looks strange, because  ⊆to  and  ⊆from  are similar and
symmetric
(and it is difficult to guess of this _,′_).

Is this a bug?

Thanks,

------
Sergei