proposition: Lemma In_umfoldlMX (f : U) (k : K) (v : V) : (k, v) \In um_foldl a Unit um_undef f -> exists k1 v1, (k, v) \In a Unit k1 v1 /\ (k1, v1) \In f.
proof: Proof. elim/um_indf: f. - by rewrite umfoldl_undef=>/In_undef. - by rewrite umfoldl0=>/In0. move=>k1 v1 f IH W P. rewrite umfoldlUn_frame // umfoldlPt (validPtUn_cond W) unitR. case/InUn=>[H|/IH [k2][v2][H2 R2]]; first by exists k1, v1. by exists k2, v2; split=>//; apply/InPtUnE=>//; right. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)