fact: Definition update (X : set Te) b := match BOrd.compare b a with | LT h => I_lt_a h | EQ _ => X | GT _ => SN R_aeq end.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)