proposition: Lemma takeord T k x (f : {ffun I -> T}) : take (indx k) (fgraph [ffun y => [eta f with k |-> x] y]) = take (indx k) (fgraph f).
proof: Proof. set f' := (finfun _). suff E: {in take (indx k) (enum I), f =1 f'}. - by rewrite !fgraph_codom /= !codomE -2!map_take; move/eq_in_map: E. move: (enum_uniq I); rewrite {1}(enum_split k) cat_uniq /= =>H4. move=>y H5; rewrite /f' /= !ffunE /=; case: eqP H5 H4=>// -> ->. by rewrite andbF. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap) mathcomp(fintype tuple finfun)