proposition: Lemma um_contra k v f g : f = pts k v \+ g \+ f -> ~~ valid f.
proof: Proof. move=>E; rewrite E -joinAC -joinA validPtUn. rewrite {2}E -!joinA domPtUn !inE. by rewrite eq_refl andbT !joinA -E andbN andbF. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)