Using a View makes proving easier

ViewExample.agda

open import Relation.Nullary
open import Agda.Builtin.Equality

data X : Set where
  a b c : X

firstA : (x y z : X) → X
firstA a y z = a
firstA x a z = a
firstA x y a = a
firstA x y z = a

firstA-id : ∀ x y z → firstA x y z ≡ a
firstA-id a y z = refl
-- firstA-id x a z = refl -- doesn't work
firstA-id b a z = refl
firstA-id c a z = refl
-- firstA-id x y a = {!refl!} -- doesn't work
firstA-id b b a = refl
firstA-id b c a = refl
firstA-id c b a = refl
firstA-id c c a = refl
firstA-id b b b = refl
firstA-id b b c = refl
firstA-id b c b = refl
firstA-id b c c = refl
firstA-id c b b = refl
firstA-id c b c = refl
firstA-id c c b = refl
firstA-id c c c = refl

-- rather than matching on the LHS on a, we can use a function
-- distinguishing two cases: a and not a.

isA : ∀ x → Dec (x ≡ a)
isA a = yes refl
isA b = no (λ ())
isA c = no (λ ())

-- The function is just as long:

firstA' : (x y z : X) → X
firstA' x y z with isA x | isA y | isA z
... | yes _ | _ | _ = a
... | _ | yes _ | _ = a
... | _ | _ | yes _ = a
... | _ | _ | _     = a

-- But the proof is vastly shorter:

firstA'-id : ∀ x y z → firstA' x y z ≡ a
firstA'-id x y z with isA x | isA y | isA z
... | yes _ | _     | _     = refl
... | no _  | yes _ | _     = refl
... | no _  | no _  | yes _ = refl
... | no _  | no _  | no _  = refl