fact: Definition um_foldl (a : R -> K -> V -> R) (z0 d : R) f := if valid f then foldl (fun z kv => a z kv.1 kv.2) z0 (assocs f) else d.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)