fact: Definition join (S1 S2: t) : t := match S1, S2 with | Bot, _ => S2 | _, Bot => S1 | Top_except m1, Top_except m2 => Top_except (IdentMap.map2 join_aux m1 m2) end.
imports: Coq(ZArith Psatz Bool String List FMaps) CDF(Sequences IMP)