∀ (name userName html name_1 userName_1 html_1 : Lean.Json),
  ({ name := name, userName := userName, html := html } = { name := name_1, userName := userName_1, html := html_1 }) =
    (name = name_1 ∧ userName = userName_1 ∧ html = html_1)