fact: Definition um_comp g f : U := um_foldl (fun r k v => if find v g is Some w then pts k w \+ r else r) Unit undef f.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)