Differential operators as a quantization of functions on the cotangent bundle As the title states, I am trying to see differential operators as a quantization of functions on the cotangent bundle. Specifically, let's assume that $k$ is a field of characteristic $0$, and $X$ is a smooth affine $k$-scheme. 
Grothendieck gives an inductive description of differential operators as follows:
$$\text{Diff}_{\le 0}(\mathcal{O}(X)) := \text{End}_{\mathcal{O}(X)}(\mathcal{O}(X)),$$
$$\text{Diff}_{\le m}(\mathcal{O}(X)) := \{ \phi \in \text{End}_{k}(\mathcal{O}(X)) ~|~ [\phi,a] \in \text{Diff}_{\le m-1} \text{ for all } a \in \mathcal{O}(X)\}.$$
Then define
$$\text{Diff}(\mathcal{O}(X)) := \bigcup \text{Diff}_{\le m}.$$
I wish to show the associated graded algebra is isomorphic to functions on the cotangent bundle:
$$\text{grDiff}(\mathcal{O}(x)) \cong \text{Sym}_{\mathcal{O}(X)}(\text{Vect}(X)),$$
where $\text{Vect}(X) = \text{Der}_{k}(\mathcal{O}(X),\mathcal{O}(X)).$
I've boiled this down to showing that when $X$ is smooth, PBW generalizes to show that the universal enveloping algebroid is a quantization of functions of the cotangent bundle, and then that there is an isomorphism between the universal enveloping algebroid and $\text{Diff}(\mathcal{O}(X)).$ 
Specifically, can someone help me see how to show the latter of these two items:
$$\mathcal{U}_{\mathcal{O}(X)}\text{Vect}(X) \cong \text{Diff}(\mathcal{O}(X)).$$
I'm not that comfortable with Lie algebroids, so that is surely part of the trouble.
 A: There is an obvious map $\mathrm{Vect}(X)\to \mathrm{Diff}_{\leq 1}\mathcal{O}_X(X)$ given by sending a derivation to the $k$-linear endomorphism it represents, and the commutator relation is immediate from the Leibniz rule (as these derivations are $\mathcal{O}_X$-linear combinations of derivatives). It remains to assemble this map into a map involving $\mathcal{U}_{\mathcal{O}_X}$ and $\mathrm{Diff}(\mathcal{O}_X(X))$.
Observation 1: Given a map of a $R$-module $M$ into an $R$-algebra $A$, we get by universal property a map from the tensor algebra $T_RM=\bigoplus M^{\otimes_R n}$ to the algebra $A$. This gives us a map $\psi:T_{\mathcal{O}_X(X)}\mathrm{Vect}(X)\to \mathrm{Diff}(\mathcal{O}_X(X))$.
Observation 2: $\psi$ vanishes on every element of the form $a\otimes b - b\otimes a - [a,b]$ where the bracket is the usual bracket on the Lie algebra $\mathrm{Der}_k(\mathcal{O}_X(X),\mathcal{O}_X(X))$. This comes from just literally writing out what these things mean. By the third isomorphism theorem, this gives us that the map $\psi$ descends to a map $\overline{\psi}:\mathcal{U}_{\mathcal{O}_X}\to \mathrm{Diff}(\mathcal{O}_X(X))$.
To prove that this map is injective, one asks whether there's anything else in the kernel of $\psi$. By playing around with the known relation, you can show that such a relation must give rise to a relation involving some element of $\mathrm{Der}_k(\mathcal{O}_X(X),\mathcal{O}_X(X))$. Similarly, to show that the map is surjective, one can take commutators on both sides with well-chosen generators to reduce to the case of the map $\mathrm{Vect}(X)\to \mathrm{Diff}_{\leq 1}\mathcal{O}_X(X)$ from earlier. So the whole verification boils down to computing these objects. Both of them are just $k[X]$-linear combinations of partial derivatives, so we obtain the result.
