fact: Definition upd k v f := if f is Def fs fpf then if decP (@idP (C k)) is left pf then Def (all_supp_insP v pf fpf) else Undef else Undef.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)