proposition: Lemma remove_one_update : forall A `{Inhab B} (m:map A B) (i:A) (v:B), (m[i:=v] \- \{i}) = (m \- \{i}).
proof: Proof. Proof using. intros. applys fun_ext_1. intros k. rewrite update_impl_eq. simpl. unfold remove_impl. do 2 case_if~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)