fact: Definition widen (s1 s2: t) : t := match s1, s2 with | Bot, _ => s2 | _, Bot => s1 | Top_except m1, Top_except m2 => Top_except (IdentMap.map2 widen_aux m1 m2) end.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)