proposition: Lemma In_umfoldlM (f : U) (k : K) (v : V) k1 v1 : valid (um_foldl a Unit um_undef f) -> (k, v) \In a Unit k1 v1 -> (k1, v1) \In f -> (k, v) \In um_foldl a Unit um_undef f.
proof: Proof. move=>W H /(In_umfoldl frame Unit um_undef) [x E]. by move: E W=>-> W; apply/InL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)