proposition: Lemma umallbP p f : reflect (forall x, x \In f -> p x) (um_allb p f).
proof: Proof. apply/(equivP idP); split=>[/eqP | H]. - by rewrite umcnt_memT=>H [k v]; apply: H. by apply/eqP; rewrite umcnt_memT=>k v; apply: H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)