proposition: Lemma setfC f k1 k2 v1 v2 : f.[k1 <- v1].[k2 <- v2] = if k2 == k1 then f.[k2 <- v2] else f.[k2 <- v2].[k1 <- v1].
proof: Proof. apply/fmapP => k. rewrite fnd_if !fnd_set. have [[->|kNk2] [// <-|k2Nk1]] // := (altP (k =P k2), altP (k2 =P k1)). by rewrite (negPf kNk2). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)