∀ (toElabInfo : Lean.Elab.ElabInfo) (mctxBefore : Lean.MetavarContext) (goalsBefore : List Lean.MVarId)
  (mctxAfter : Lean.MetavarContext) (goalsAfter : List Lean.MVarId),
  sizeOf
      { toElabInfo := toElabInfo, mctxBefore := mctxBefore, goalsBefore := goalsBefore, mctxAfter := mctxAfter,
        goalsAfter := goalsAfter } =
    1 + sizeOf toElabInfo + sizeOf mctxBefore + sizeOf goalsBefore + sizeOf mctxAfter + sizeOf goalsAfter