proposition: Lemma binds_update_inv : 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. introv H. rewrite~ binds_update_eq in H. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)