∀ (splitDisjunctions splitNatSub splitNatAbs splitMinMax : Bool),
  sizeOf
      { splitDisjunctions := splitDisjunctions, splitNatSub := splitNatSub, splitNatAbs := splitNatAbs,
        splitMinMax := splitMinMax } =
    1 + sizeOf splitDisjunctions + sizeOf splitNatSub + sizeOf splitNatAbs + sizeOf splitMinMax