proposition: Lemma umfoldr_ind (P : R -> Prop) a z0 d f : valid f -> P z0 -> (forall z0 k v, (k, v) \In f -> P z0 -> P (a k v z0)) -> P (um_foldr a z0 d f).
proof: Proof. move=>W H1 H2; elim/um_indb: f z0 W H1 H2=>[||k v f IH W /allP O] z0; rewrite ?valid_undef ?umfoldr0 // => _ H1 H2. rewrite joinC umfoldrUnPt //; rewrite joinC in W. 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)