{P : Sort u} →
  {splitDisjunctions splitNatSub splitNatAbs splitMinMax splitDisjunctions' splitNatSub' splitNatAbs' splitMinMax' :
      Bool} →
    { splitDisjunctions := splitDisjunctions, splitNatSub := splitNatSub, splitNatAbs := splitNatAbs,
          splitMinMax := splitMinMax } =
        { splitDisjunctions := splitDisjunctions', splitNatSub := splitNatSub', splitNatAbs := splitNatAbs',
          splitMinMax := splitMinMax' } →
      (splitDisjunctions = splitDisjunctions' →
          splitNatSub = splitNatSub' → splitNatAbs = splitNatAbs' → splitMinMax = splitMinMax' → P) →
        P