proposition: Lemma indom_single_eq : forall A B (x1 x2:A) (v:B), x2 \indom (x1\:=v) = (x1 = x2).
proof: Proof. Proof using. intros. rewrite dom_single. rewrite in_single_eq. extens*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)