Definition boundsWellFormed (b : boundsT) : Prop :=
     (boundsXOrder b)
  /\ (boundsYOrder b)
  /\ (boundsZOrder b)
  .
