proposition: Lemma umfoldl_defE a z0 d1 d2 f : valid f -> um_foldl a z0 d1 f = um_foldl a z0 d2 f.
proof: Proof. move: f z0; elim/um_indf=>[z0|z0|k v f IH W /(order_path_min (@trans K)) P z0 _]; by rewrite ?valid_undef ?umfoldl0 // !umfoldlPtUn // IH // (validR W). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)