proposition: Lemma mem_setf V (f : {fmap K -> V}) (k0 : K) (v0 : V) : f.[k0 <- v0] =i predU1 k0 (mem (domf f)).
proof: Proof. by move=> k; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)