proposition: Lemma eval_ind {P : R -> Prop} f p a z0 : P z0 -> (forall k v z0, (k, v) \In f -> p (k, v) -> P z0 -> P (a z0 k v)) -> P (eval a p f z0).
proof: Proof. move=>Z H; elim/um_indf: f z0 Z H=>[||k v h IH W T] z0 Z H; rewrite ?eval_undef ?eval0 // evalPtUn // ?(order_path_min (@trans K) T) //. by apply: IH=>[|k0 v0 z1 /(InR W)]; [case: ifP=>Pk //=; apply: H | apply: H]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)