proposition: Lemma umcnt_memT p f : um_count p f = size (dom f) <-> forall k v, (k, v) \In f -> p (k, v).
proof: Proof. elim/um_indf: f=>[||k v f IH W P]. - by rewrite umcnt_undef dom_undef; split=>// _ k v /In_undef. - by rewrite umcnt0 dom0; split=>// _ k v /In0. rewrite umcntPtUn // size_domPtUn //. case: ifP=>H; split. - move/eqP; rewrite !add1n eqSS=>/eqP/IH=>H1 k1 v1. by case/InPtUnE=>//; [case=>->-> | apply: H1]. - move=>H1; apply/eqP; rewrite !add1n eqSS; apply/eqP. by apply/IH=>k1 v1 H2; apply: H1; apply/InR. - by rewrite add0n=>X; move: (umcnt_size p f); rewrite X add1n ltnn. by move/(_ k v)/(_ (InPtUnL W)); rewrite H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)