proposition: Lemma eq_in_umcnt2 p1 p2 f : p1 =1 p2 -> um_count p1 f = um_count p2 f.
proof: Proof. by move=>S; apply: eq_in_umcnt=>kv _; apply: S. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)