proposition: Lemma setfK V (f : {fmap K -> V}) k0 v0 (x : domf f.[k0 <- v0]): f.[k0 <- v0] x = if (val x != k0) =P true isn't ReflectT xNk0 then v0 else f.[fnd_set_in xNk0].
proof: Proof. case: eqP => [p|]; rewrite ?ffunE/=; last by case: (altP eqP). by rewrite (negPf p) in_fnd ?fnd_set_in// => xf; apply: eq_getf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)