proposition: Lemma read_remove_one_neq : forall A `{Inhab B} (M:map A B) i j, i <> j -> (M\--i)[j] = M[j].
proof: Proof. Proof using. introv N. simpl. unfold remove_impl, read_impl. case_if~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)