proposition: Lemma eq_in_umcnt p1 p2 f : (forall kv, kv \In f -> p1 kv = p2 kv) -> um_count p1 f = um_count p2 f.
proof: Proof. by rewrite /um_count=>/eq_in_umfilt ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)