proposition: Lemma umpreimPt p k v : C k -> um_preim p (pts k v) =1 [pred x | (x == k) && p v].
proof: Proof. move=>Hk x; rewrite /um_preim /= findPt2. by case: eqP=>//= _; rewrite Hk. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)