proposition: Lemma rangePtK k v : C k -> range (U:=U) (pts k v) = [:: v].
proof: Proof. by move=>C'; rewrite /range assocsPt C'. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)