proposition: Lemma eval_pred0 a z0 f : eval a xpred0 f z0 = z0.
proof: Proof. case W : (valid f); last first. - by move/negbT/invalidE: W=>->; rewrite eval_undef. by rewrite /eval umfilt_pred0 // dom0 /=. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)