proposition: Lemma umall2_umcnt f1 f2 p : (forall k v1 v2, (k, v1) \In f1 -> (k, v2) \In f2 -> P v1 v2 -> p (k, v1) = p (k, v2)) -> um_all2 f1 f2 -> um_count p f1 = um_count p f2.
proof: Proof. by move=>*; congr size; apply: umall2_dom; apply: umall2_umfilt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)