proposition: Lemma dom_umcomp_sub g f : {subset dom (um_comp g f) <= dom f}.
proof: Proof. rewrite /um_comp; elim/um_indf: f=>[||k v f IH W P] x. - by rewrite umfoldl_undef dom_undef. - by rewrite umfoldl0 dom0. rewrite umfoldlUn_frame //; last by move=>*; case: (find _ _)=>// a; rewrite joinA. rewrite unitR umfoldlPt (validPtUn_cond W). case E : (find v g)=>[b|]; last first. - by rewrite unitL=>/IH; rewrite domPtUn inE W =>->; rewrite orbT. rewrite unitR domPtUn inE; case/andP=>_ /orP [/eqP <-|/IH]. - by rewrite domPtUn inE W eq_refl. by rewrite domPtUn inE W=>->; rewrite orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)