proposition: Lemma eq_filt_eval a p1 p2 z0 f1 f2 : um_filter p1 f1 = um_filter p2 f2 -> eval a p1 f1 z0 = eval a p2 f2 z0.
proof: Proof. by rewrite !eval_oevUmfilt=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)