proposition: Lemma eval_ind2 {P : R1 -> R2 -> Prop} (f : U) p0 p1 a0 a1 z0 z1 : P z0 z1 -> (forall k v z0 z1, (k, v) \In f -> P z0 z1 -> P (if p0 (k, v) then a0 z0 k v else z0) (if p1 (k, v) then a1 z1 k v else z1)) -> P (eval a0 p0 f z0) (eval a1 p1 f z1).
proof: Proof. move=>Z H; elim/um_indf: f z0 z1 Z H=>[||k v h IH W T] z0 z1 Z H; rewrite ?eval_undef ?eval0 // !evalPtUn // ?(order_path_min (@trans K) T) //=. apply: IH; first by case: ifPn (H k v z0 z1 (InPtUnL W) Z). by move=>k0 v0 w1 w2 X; apply: H (InR W X). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)