proposition: Lemma valid_umcomp g f : valid (um_comp g f) = valid f.
proof: Proof. rewrite /um_comp; elim/um_indf: f=>[||k v f IH W P]. - by rewrite umfoldl_undef !valid_undef. - by rewrite umfoldl0 !valid_unit. rewrite umfoldlUn_frame //; last by move=>*; case: (find _ _)=>// a; rewrite joinA. rewrite unitR W umfoldlPt (validPtUn_cond W). case: (find v g)=>[a|]; last by rewrite unitL IH (validR W). rewrite unitR validPtUn (validPtUn_cond W) IH (validR W). by apply: contra (notin_path P); apply: dom_umcomp_sub. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)