∀ {ngen : Lean.NameGenerator} {lctx : Lean.LocalContext} {mctx : Lean.MetavarContext} {nextParamIdx : ℕ}
  {paramNames : Array Lean.Name} {fvars mvars : Array Lean.Expr} {lmap : Std.HashMap Lean.LMVarId Lean.Level}
  {emap : Std.HashMap Lean.MVarId Lean.Expr} {abstractLevels : Bool} {ngen_1 : Lean.NameGenerator}
  {lctx_1 : Lean.LocalContext} {mctx_1 : Lean.MetavarContext} {nextParamIdx_1 : ℕ} {paramNames_1 : Array Lean.Name}
  {fvars_1 mvars_1 : Array Lean.Expr} {lmap_1 : Std.HashMap Lean.LMVarId Lean.Level}
  {emap_1 : Std.HashMap Lean.MVarId Lean.Expr} {abstractLevels_1 : Bool},
  { ngen := ngen, lctx := lctx, mctx := mctx, nextParamIdx := nextParamIdx, paramNames := paramNames, fvars := fvars,
        mvars := mvars, lmap := lmap, emap := emap, abstractLevels := abstractLevels } =
      { ngen := ngen_1, lctx := lctx_1, mctx := mctx_1, nextParamIdx := nextParamIdx_1, paramNames := paramNames_1,
        fvars := fvars_1, mvars := mvars_1, lmap := lmap_1, emap := emap_1, abstractLevels := abstractLevels_1 } →
    ngen = ngen_1 ∧
      lctx = lctx_1 ∧
        mctx = mctx_1 ∧
          nextParamIdx = nextParamIdx_1 ∧
            paramNames = paramNames_1 ∧
              fvars = fvars_1 ∧ mvars = mvars_1 ∧ lmap = lmap_1 ∧ emap = emap_1 ∧ abstractLevels = abstractLevels_1