∀ {declName : Lean.Name} {levelParams : List Lean.Name} {type value : Lean.Expr} {declNames : Array Lean.Name}
  {declNameNonRec : Lean.Name} {fixedParamPerms : Lean.Elab.FixedParamPerms}
  {fixpointType : Array Lean.Elab.PartialFixpointType} {declName_1 : Lean.Name} {levelParams_1 : List Lean.Name}
  {type_1 value_1 : Lean.Expr} {declNames_1 : Array Lean.Name} {declNameNonRec_1 : Lean.Name}
  {fixedParamPerms_1 : Lean.Elab.FixedParamPerms} {fixpointType_1 : Array Lean.Elab.PartialFixpointType},
  { declName := declName, levelParams := levelParams, type := type, value := value, declNames := declNames,
        declNameNonRec := declNameNonRec, fixedParamPerms := fixedParamPerms, fixpointType := fixpointType } =
      { declName := declName_1, levelParams := levelParams_1, type := type_1, value := value_1,
        declNames := declNames_1, declNameNonRec := declNameNonRec_1, fixedParamPerms := fixedParamPerms_1,
        fixpointType := fixpointType_1 } →
    declName = declName_1 ∧
      levelParams = levelParams_1 ∧
        type = type_1 ∧
          value = value_1 ∧
            declNames = declNames_1 ∧
              declNameNonRec = declNameNonRec_1 ∧ fixedParamPerms = fixedParamPerms_1 ∧ fixpointType = fixpointType_1