proposition: Lemma In_assocs f x : x \In assocs f <-> x \In f.
proof: Proof. move: f; apply: um_indf=>[||k v f IH W /(order_path_min (@trans K)) P]. - by rewrite assocs_undef; split=>// /In_undef. - by rewrite assocs0; split=>// /In0. by rewrite assocsPtUn ?InE // InPtUnE // IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)