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