proposition: Lemma binds_update_neq_inv : forall A B i j v w (M:map A B), binds (M[j:=w]) i v -> i <> j -> binds M i v.
proof: Proof. Proof using. introv H N. asserts IB: (Inhab B). constructor. exists* v. rewrite (@binds_eq_indom_read A B IB) in *. rewrite~ indom_update_eq in H. rewrite* read_update_neq in H. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)