∀ {toConstantVal : Lean.ConstantVal} {numParams numIndices : ℕ} {all ctors : List Lean.Name} {numNested : ℕ}
  {isRec isUnsafe isReflexive : Bool} {toConstantVal_1 : Lean.ConstantVal} {numParams_1 numIndices_1 : ℕ}
  {all_1 ctors_1 : List Lean.Name} {numNested_1 : ℕ} {isRec_1 isUnsafe_1 isReflexive_1 : Bool},
  { toConstantVal := toConstantVal, numParams := numParams, numIndices := numIndices, all := all, ctors := ctors,
        numNested := numNested, isRec := isRec, isUnsafe := isUnsafe, isReflexive := isReflexive } =
      { toConstantVal := toConstantVal_1, numParams := numParams_1, numIndices := numIndices_1, all := all_1,
        ctors := ctors_1, numNested := numNested_1, isRec := isRec_1, isUnsafe := isUnsafe_1,
        isReflexive := isReflexive_1 } →
    toConstantVal = toConstantVal_1 ∧
      numParams = numParams_1 ∧
        numIndices = numIndices_1 ∧
          all = all_1 ∧
            ctors = ctors_1 ∧
              numNested = numNested_1 ∧ isRec = isRec_1 ∧ isUnsafe = isUnsafe_1 ∧ isReflexive = isReflexive_1