proposition: Lemma eq_in_umfiltE p1 p2 f : p1 =1 p2 -> um_filter p1 f = um_filter p2 f.
proof: Proof. by move=>S; apply/eq_in_umfilt=>kv _; apply: S. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)