proposition: Lemma umallPtUnE k v f : valid (pts k v \+ f) -> um_all (pts k v \+ f) -> P k v /\ um_all f.
proof: Proof. move=>W H; move: (umallUnL W H) (umallUnR W H)=>{H} H1 H2. by split=>//; apply: umallPtE H1; apply: validPtUn_cond W. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)