proposition: Lemma eq_in_eval p q z0 f a : (forall kv, kv \In f -> p kv = q kv) -> eval a p f z0 = eval a q f z0.
proof: Proof. by rewrite (eval_umfilt p) (eval_umfilt q); 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)