proposition: Lemma find_omf f k h : find k (f h) = if find k h is Some v then map_fun f (k, v) else None.
proof: Proof. by case: f=>s [m H] /=; rewrite H find_omap. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)