proposition: Lemma findF k1 k2 f : find k1 (free f k2) = if k1 == k2 then None else find k1 f.
proof: Proof. rewrite !umEX /UM.find /UM.free. case: (UMC.from f)=>[|f' F]; first by rewrite if_same. by 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)