proposition: Lemma updi_split T k (f : {ffun I -> T}) : updi p (fgraph f) = updi p (take (indx k) (fgraph f)) \+ p.+(indx k) :-> f k \+ updi (p.+(indx k).+1) (drop (indx k).+1 (fgraph f)).
proof: Proof. rewrite fgraph_codom /= codomE {1}(enum_split k) map_cat updi_cat /=. rewrite map_take map_drop size_takel ?joinA ?ptrA ?addn1 //. by rewrite size_map index_size. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap) mathcomp(fintype tuple finfun)