proposition: Lemma umcompfPtUn g f k v : valid (pts k v \+ f) -> um_comp g (pts k v \+ f) = if find v g is Some w then pts k w \+ um_comp g f else um_comp g f.
proof: Proof. move=>W; rewrite umcompfUn // umcompfPt (validPtUn_cond W). by case: (find _ _)=>[a|] //; rewrite unitL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)