proposition: Lemma update_remove_one_neq : forall A B (M:map A B) i j v, i <> j -> (M\--i)[j:=v] = (M[j:=v] \--i).
proof: Proof. Proof using. introv N. applys fun_ext_1. intros k. do 2 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)