∀ {levelNames : List Lean.Name} {syntheticMVars : Lean.MVarIdMap Lean.Elab.Term.SyntheticMVarDecl}
  {pendingMVars : List Lean.MVarId} {mvarErrorInfos : List Lean.Elab.Term.MVarErrorInfo}
  {levelMVarErrorInfos : List Lean.Elab.Term.LevelMVarErrorInfo} {mvarArgNames : Lean.MVarIdMap Lean.Name}
  {letRecsToLift : List Lean.Elab.Term.LetRecToLift} {levelNames_1 : List Lean.Name}
  {syntheticMVars_1 : Lean.MVarIdMap Lean.Elab.Term.SyntheticMVarDecl} {pendingMVars_1 : List Lean.MVarId}
  {mvarErrorInfos_1 : List Lean.Elab.Term.MVarErrorInfo}
  {levelMVarErrorInfos_1 : List Lean.Elab.Term.LevelMVarErrorInfo} {mvarArgNames_1 : Lean.MVarIdMap Lean.Name}
  {letRecsToLift_1 : List Lean.Elab.Term.LetRecToLift},
  { levelNames := levelNames, syntheticMVars := syntheticMVars, pendingMVars := pendingMVars,
        mvarErrorInfos := mvarErrorInfos, levelMVarErrorInfos := levelMVarErrorInfos, mvarArgNames := mvarArgNames,
        letRecsToLift := letRecsToLift } =
      { levelNames := levelNames_1, syntheticMVars := syntheticMVars_1, pendingMVars := pendingMVars_1,
        mvarErrorInfos := mvarErrorInfos_1, levelMVarErrorInfos := levelMVarErrorInfos_1,
        mvarArgNames := mvarArgNames_1, letRecsToLift := letRecsToLift_1 } →
    levelNames = levelNames_1 ∧
      syntheticMVars = syntheticMVars_1 ∧
        pendingMVars = pendingMVars_1 ∧
          mvarErrorInfos = mvarErrorInfos_1 ∧
            levelMVarErrorInfos = levelMVarErrorInfos_1 ∧
              mvarArgNames = mvarArgNames_1 ∧ letRecsToLift = letRecsToLift_1