proposition: Lemma umfoldlUn_frame z0 d (f1 f2 : U) : valid (f1 \+ f2) -> um_foldl a z0 d (f1 \+ f2) = um_foldl a Unit d f1 \+ um_foldl a Unit d f2 \+ z0.
proof: Proof. move=>W; rewrite /um_foldl W (validL W) (validR W). set b := fun z kv => _. have X x y kv : b (x \+ y) kv = b x kv \+ y by rewrite /b frame. rewrite (foldl_perm X _ (assocs_perm W)). rewrite foldl_cat -{1}[z0]unitL (foldl_init X). rewrite (foldl_init X) -{1}[foldl b _ (assocs f1)]unitL. by rewrite (foldl_init X) -!joinA joinCA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)