proposition: Lemma umcompfPt g k v : um_comp g (pts k v) = if C1 k then if find v g is Some w then pts k w else Unit else undef.
proof: Proof. rewrite /um_comp umfoldlPt; case: ifP=>C //. by case: (find _ _)=>// a; rewrite unitR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)