[Agda] a puzzle about pattern matching

[effectfully]

Matteo Acerbi, in this case it's easier to just use decidable equality:

open import Relation.Nullary
open import Relation.Binary

postulate
  _≟A_ : Decidable (_≡_ {A = A})

action : A → A
action x with x ≟A d a a a
... | yes _  = d a a a
... | no  _  = a

lem : ∀(x : A) → x ≢ d a a a → action x ≡ a
lem x c with x ≟A d a a a
... | yes p = ⊥-elim (c p)
... | no  _ = refl