proposition: Lemma eq_in_umfiltk p1 p2 f : {in dom f, p1 =1 p2} -> um_filterk p1 f = um_filterk p2 f.
proof: Proof. by move=>H; apply/eq_in_umfilt; case=>k v /In_dom; apply: H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)