∀ (name : Lean.Name) (declName? : Option Lean.Name) (numFields : ℕ) (provesMotive : Bool),
  sizeOf { name := name, declName? := declName?, numFields := numFields, provesMotive := provesMotive } =
    1 + sizeOf name + sizeOf declName? + sizeOf numFields + sizeOf provesMotive