proposition: Lemma eq_in_umfiltI p1 p2 f : (forall kv, kv \In f -> p1 kv = p2 kv) -> um_filter p1 f = um_filter p2 f.
proof: Proof. by move/eq_in_umfilt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)