proposition: Lemma dom_setf V (f : {fmap K -> V}) (k0 : K) (v0 : V) : domf (f.[k0 <- v0]) = k0 |` domf f.
proof: Proof. by apply/fsetP=> k; rewrite mem_setf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)