proposition: Lemma eq_in_umfilt p1 p2 f : (forall kv, kv \In f -> p1 kv = p2 kv) <-> um_filter p1 f = um_filter p2 f.
proof: Proof. split. - by move=> H; apply /eq_in_omap => kv In; rewrite H. move=>H x [W][z E]; subst f. rewrite !umfiltPtUn W -prod_eta in H. case: ifP H; case: ifP=>// H1 H2 E. - have: x.1 \in dom (um_filter p2 z). - by rewrite -E domPtUn inE E eq_refl valid_umfilt (validR W). by move/dom_umfilt_subset; rewrite (negbTE (validPtUnD W)). have: x.1 \in dom (um_filter p1 z). - by rewrite E domPtUn inE -E eq_refl valid_umfilt (validR W). by move/dom_umfilt_subset; rewrite (negbTE (validPtUnD W)). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)