proposition: Remark measure_map_empty: forall m, IdentMap.Empty m -> measure_map m = 0%nat.
proof: Proof. intros. apply IMProp.fold_Empty; auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)