∀ {kind : String} {message? : Option String} {kind_1 : String} {message?_1 : Option String},
  { kind := kind, message? := message? } = { kind := kind_1, message? := message?_1 } →
    kind = kind_1 ∧ message? = message?_1