fact: Definition set (x: ident) (N: V.t) (S: t): t := if V.ble N V.bot then Bot else match S with | Bot => Bot | Top_except m => Top_except (IdentMap.add x N m) end.
imports: Coq(ZArith Psatz Bool String List FMaps) CDF(Sequences IMP)