∀ {type : Lean.Expr} {structNameSet : Lean.NameSet} {fieldMap : Lean.NameMap Lean.Expr} {fields : Array Lean.Expr}
  {instMVars : Array Lean.MVarId} {liftedFVars : Array Lean.Expr} {liftedFVarRemap : Lean.FVarIdMap Lean.FVarId}
  {optParamFields : Array (Lean.Name × Lean.Expr × Bool)} {type_1 : Lean.Expr} {structNameSet_1 : Lean.NameSet}
  {fieldMap_1 : Lean.NameMap Lean.Expr} {fields_1 : Array Lean.Expr} {instMVars_1 : Array Lean.MVarId}
  {liftedFVars_1 : Array Lean.Expr} {liftedFVarRemap_1 : Lean.FVarIdMap Lean.FVarId}
  {optParamFields_1 : Array (Lean.Name × Lean.Expr × Bool)},
  { type := type, structNameSet := structNameSet, fieldMap := fieldMap, fields := fields, instMVars := instMVars,
        liftedFVars := liftedFVars, liftedFVarRemap := liftedFVarRemap, optParamFields := optParamFields } =
      { type := type_1, structNameSet := structNameSet_1, fieldMap := fieldMap_1, fields := fields_1,
        instMVars := instMVars_1, liftedFVars := liftedFVars_1, liftedFVarRemap := liftedFVarRemap_1,
        optParamFields := optParamFields_1 } →
    type = type_1 ∧
      structNameSet = structNameSet_1 ∧
        fieldMap = fieldMap_1 ∧
          fields = fields_1 ∧
            instMVars = instMVars_1 ∧
              liftedFVars = liftedFVars_1 ∧ liftedFVarRemap = liftedFVarRemap_1 ∧ optParamFields = optParamFields_1