proposition: Lemma validPtUn k v f : valid (pts k v \+ f) = [&& C k, valid f & k \notin dom f].
proof: Proof. case: validUn=>//; last 1 first. - rewrite validPt=>H1 -> H2; rewrite H1 (H2 k) //. by rewrite domPtK H1 inE. - by rewrite validPt; move/negbTE=>->. - by move/negbTE=>->; rewrite andbF. rewrite domPtK=>x; case: ifP=>// _. by rewrite inE=>/eqP ->->; rewrite andbF. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)