∀ (elabs : Array Lean.Elab.Command.InductiveElabStep2) (mctx : Lean.MetavarContext) (levelParams : List Lean.Name)
  (params : Array Lean.Expr) (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances)
  (replaceIndFVars : Lean.Expr → Lean.MetaM Lean.Expr),
  sizeOf
      { elabs := elabs, mctx := mctx, levelParams := levelParams, params := params, lctx := lctx,
        localInsts := localInsts, replaceIndFVars := replaceIndFVars } =
    1 + sizeOf elabs + sizeOf mctx + sizeOf levelParams + sizeOf params + sizeOf lctx + sizeOf localInsts