∀ (toElabInfo : Lean.Elab.ElabInfo) (lctx : Lean.LocalContext) (expectedType? : Option Lean.Expr),
  sizeOf { toElabInfo := toElabInfo, lctx := lctx, expectedType? := expectedType? } =
    1 + sizeOf toElabInfo + sizeOf lctx + sizeOf expectedType?