∀ (nextIdx : ℕ) (lmap : Std.HashMap Lean.LMVarId Lean.Level) (emap : Std.HashMap Lean.MVarId Lean.Expr)
  (mctx : Lean.MetavarContext),
  sizeOf { nextIdx := nextIdx, lmap := lmap, emap := emap, mctx := mctx } =
    1 + sizeOf nextIdx + sizeOf lmap + sizeOf emap + sizeOf mctx