proposition: Lemma In_rangePtUn k v f x : valid (pts k v \+ f) -> x \In range (pts k v \+ f) <-> x = v \/ x \In range f.
proof: Proof. move=>W; split. - case/In_rangeUn; last by right. by move/(In_rangePt (validPtUn_cond W)); left. case=>[->|]; last by apply: In_rangeR. by apply/(In_rangeL W)/(In_rangePt (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)