proposition: Lemma dom_find k f : dom_find_spec k f (k \in dom f).
proof: Proof. rewrite !umEX /UM.dom -{1}[f]UMC.tfE. case: (UMC.from f)=>[|f' H]. - by apply: dom_find_none'; rewrite !umEX. case: suppP (allP H k)=>[v|] H1 I; last first. - by apply: dom_find_none'; rewrite !umEX. apply: (dom_find_some' (v:=v)); rewrite !umEX // /UM.upd /UM.free. case: decP=>H2; last by rewrite I in H2. apply/fmapP=>k'; rewrite fnd_ins. by case: ifP=>[/eqP-> //|]; rewrite fnd_rem => ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)