∀ (data name : Array Lean.Json) (length : ℕ) (data_1 name_1 : Array Lean.Json) (length_1 : ℕ),
  ({ data := data, name := name, length := length } = { data := data_1, name := name_1, length := length_1 }) =
    (data = data_1 ∧ name = name_1 ∧ length = length_1)