# Pastebin NYnrRS7L
open import Agda.Builtin.String
open import Agda.Builtin.TrustMe

_≟_ : (s s′ : String) → Dec (s ≡ s′)
s ≟ s′ with primStringEquality s s′
...    | true  = yes primTrustMe
...    | false = no s≢s′
  where
    postulate
      s≢s′ : s ≢ s′