∀ {parents : Array Lean.Elab.Command.Structure.StructParentInfo}
  {fields : Array Lean.Elab.Command.Structure.StructFieldInfo} {fieldIdx ancestorFieldIdx : Lean.NameMap ℕ}
  {fvarIdFieldIdx : Lean.FVarIdMap ℕ} {parents_1 : Array Lean.Elab.Command.Structure.StructParentInfo}
  {fields_1 : Array Lean.Elab.Command.Structure.StructFieldInfo} {fieldIdx_1 ancestorFieldIdx_1 : Lean.NameMap ℕ}
  {fvarIdFieldIdx_1 : Lean.FVarIdMap ℕ},
  { parents := parents, fields := fields, fieldIdx := fieldIdx, ancestorFieldIdx := ancestorFieldIdx,
        fvarIdFieldIdx := fvarIdFieldIdx } =
      { parents := parents_1, fields := fields_1, fieldIdx := fieldIdx_1, ancestorFieldIdx := ancestorFieldIdx_1,
        fvarIdFieldIdx := fvarIdFieldIdx_1 } →
    parents = parents_1 ∧
      fields = fields_1 ∧
        fieldIdx = fieldIdx_1 ∧ ancestorFieldIdx = ancestorFieldIdx_1 ∧ fvarIdFieldIdx = fvarIdFieldIdx_1