proposition: Lemma dom_remove_one : forall A B i (M:map A B), dom (M\--i) = dom M \- \{i}.
proof: Proof. Proof using. intros. applys~ dom_remove. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)