proposition: Lemma rangePtUn k v f : range (pts k v \+ f) =i [pred x | valid (pts k v \+ f) & (v == x) || (x \in range f)].
proof: Proof. move=>x; rewrite rangeUn !inE; case W : (valid _)=>//=. by rewrite rangePt ?(validPtUn_cond W) // eq_sym. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)