proposition: Lemma find_cond k f : ~~ C k -> find k f = None.
proof: Proof. simpl. rewrite !umEX /UM.find; case: (UMC.from f)=>[|f' F] // H. suff: k \notin supp f' by case: suppP. by apply: contra H; case: allP F=>// F _ /F. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)