proposition: Lemma In_umfoldl z0 d (f : U) (k : K) (v : V) : (k, v) \In f -> [pcm a Unit k v <= um_foldl a z0 d f].
proof: Proof. move=>H; move: (H); rewrite (In_eta H); case=>W _. by rewrite umfoldlUn_frame // umfoldlPt (validPtUn_cond W) /= -joinA; eauto. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)