proposition: Lemma index_remove_one_in : forall A B i j (M:map A B), index M j -> i <> j -> index (M\--i) j.
proof: Proof. Proof using. introv R N. rewrite index_eq_indom in *. rewrite dom_remove_one. rew_set. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)