proposition: Lemma eq_in_umfiltv (q1 q2 : pred V) f : (forall v, v \In range f -> q1 v = q2 v) -> um_filterv q1 f = um_filterv q2 f.
proof: Proof. by move=>H; apply/eq_in_umfilt; case=>k v /In_range; apply: H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)