proposition: Lemma umfoldl_ind (P : R -> Prop) a z0 d f : valid f -> P z0 -> (forall z0 k v, (k, v) \In f -> P z0 -> P (a z0 k v)) -> P (um_foldl a z0 d f).
proof: Proof. move=>W H1 H2; elim/um_indf: f z0 W H1 H2=>[||k v f IH W O] z0; rewrite ?valid_undef ?umfoldl0 // => _ H1 H2; rewrite umfoldlPtUn //; last by apply: order_path_min O; apply: trans. apply: IH (validR W) _ _; first by apply: H2 (InPtUnL W) H1. by move=>z1 k0 v0 F; apply: H2 (InR W F). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)