fact: Definition ble (S1 S2: t) : bool := match S1, S2 with | Bot, _ => true | _, Bot => false | Top_except m1, Top_except m2 => IMProp.for_all (fun x v => V.ble (get x S1) v) m2 end.
imports: Coq(ZArith Psatz Bool String List FMaps) CDF(Sequences IMP)