proposition: Lemma In_find k v f : (k, v) \In f <-> find k f = Some v.
proof: Proof. split=>[[W] /= [z E]|E]; first by rewrite E findPtUn // -E. split; first by move/find_some/dom_valid: E. by move/um_eta2: E=>->; exists (free f k). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)