proposition: Lemma umfiltkPtUn p k v f : um_filterk p (pts k v \+ f) = if valid (pts k v \+ f) then if p k then pts k v \+ um_filterk p f else um_filterk p f else undef.
proof: Proof. case: ifP=>X; last by move/invalidE: (negbT X)=>->; rewrite umfilt_undef. rewrite umfiltUn // umfiltPt (validPtUn_cond X) /=. by case: ifP=>//; rewrite unitL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)