proposition: Lemma fsfun_withE f x y z : [fsfun f with x |-> y] z = if z == x then y else f z.
proof: Proof. by rewrite fsfunE !inE/= mem_finsupp; case: eqP; case: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)