deniok

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ x → x ≡ x

data _≐_ {A : Set} (x : A) : A → Set where
  refl' : x ≐ x

lem1 : {A : Set} (x y : A) →  x ≡ y → x ≐ y
lem1 x .x (refl .x) = refl'

lem2 : {A : Set} (x y : A) →  x ≐ y → x ≡ y
lem2 x .x refl' = refl x

:)

Конфлюэнтность же никто не отменял. Тайпчекер приводит то, что требуется уравнять, к нормальной форме, тупо пользуясь definitional equality там, где это возможно, и сравнивает. В первом случае от делает это в трех местах

ex : (x : ℕ) → zero + suc x ≡ suc (zero + x)
ex x = refl (zero + zero + suc x)

, а во втором в двух. Но нормальная форма единственна (suc x), поэтому разницы нет.