fact: Definition measure_map (m: IdentMap.t V.t) : nat := IdentMap.fold (fun x v n => (V.measure v + n)%nat) m 0%nat.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)