proposition: Lemma omfPt f k e : C k -> f (pts k e) = if map_fun f (k, e) is Some v then pts k v else Unit.
proof: Proof. by case: f=>s [m X] /= N; rewrite X omapPt /= N. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)