∀ (summary sinceVersion : String) (severity : Lean.MessageSeverity) (removedVersion? : Option String),
  sizeOf
      { summary := summary, sinceVersion := sinceVersion, severity := severity, removedVersion? := removedVersion? } =
    1 + sizeOf summary + sizeOf sinceVersion + sizeOf severity + sizeOf removedVersion?