proposition: Lemma umcnt_eval p f : um_count p f = eval (fun n _ _ => n.+1) p f 0.
proof: Proof. elim/um_indf: f=>[||k v f IH W /(order_path_min (@trans K)) P]. - by rewrite umcnt_undef eval_undef. - by rewrite umcnt0 eval0. rewrite umcntPtUn // evalPtUn //=; case: ifP=>// H. by rewrite /eval oev1 // IH addnC; congr (_ + _). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)