proposition: Lemma umallUnPt k v f : P k v -> um_all f -> um_all (f \+ pts k v).
proof: Proof. by rewrite joinC; apply: umallPtUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)