proposition: Lemma ummonoPtUn k' v' f : valid (pts k' v' \+ f) -> (forall k v, (k, v) \In f -> ord k k' /\ ord v v') -> um_mono (pts k' v' \+ f) = um_mono f.
proof: Proof. move=>W H; apply/idP/idP=>/ummonoP X; apply/ummonoP=>x x' w w' Y Y'. - by apply: X; apply/InR. case/(InPtUnE _ W): Y'=>[[->->]|]; case/(InPtUnE _ W): Y=>[[->->]|]; by [rewrite irr|case/H|case/H; case: ordP|apply: X]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)