Decidable equality of data types in Agda

Question

I am trying to prove decidable equality of a data type in Agda using the Agda stdlib. I have the following code, but I am unsure what to fill in the hole. The goal seems to make sense, but actually constructing it is challenging.

Is this possible in Agda and are there any ideas on how to solve this?

open import Data.String as String hiding (_≟_)

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module Problem1 where

data Test : Set where
  test : String → Test


infix 4 _≟_ 
_≟_ : Decidable {A = Test} _≡_
test x ≟ test x₁ with x String.≟ x₁
... | yes refl = yes refl
... | no ¬a = no {!!}

The hole:

Goal: ¬ test x ≡ test x₁
————————————————————————————————————————————————————————————
¬a : ¬ x ≡ x₁
x₁ : ℕ
x  : ℕ

Answer 1

This is actually a one liner, relying on case splitting over the equality proof inside an anonymous function, as follows:

... | no ¬a = no λ {refl → ¬a refl}