proposition: Lemma binds_update_eq : forall A B i j v w (M:map A B), binds (M[j:=w]) i v = (If i = j then v = w else binds M i v).
proof: Proof. Proof using. intros. applys prop_ext. iff H. { case_if. { subst. applys* binds_update_same_inv. } { applys* binds_update_neq_inv. } } { case_if. { subst. applys* binds_update_same. } { applys* binds_update_neq. } } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)