[proofplan]
We construct the parametrix at the level of full semiclassical symbols. After choosing a cutoff supported in the elliptic region and equal to $1$ on the smaller microlocal region, the ellipticity of $a_m$ gives an initial inverse symbol $b_0=\chi a_m^{-1}$. The semiclassical symbolic composition formula is then used recursively to remove each successive power of $h$ in the error. Borel summation produces a full symbol $b$, and quantizing $b$ gives a left parametrix; the same symbolic construction gives a right parametrix. Since both compositions have full symbol equal to $1$ modulo $h^\infty S^{-\infty}$ on $V$, their operator remainders are rapidly smoothing microlocally on $V$.
[/proofplan]
[step:Choose a cutoff inside the elliptic region]
Fix an open set $V \subset T^*X$ such that $\overline{V}$ is compact and $\overline{V} \subset U$. Choose a cutoff
\begin{align*} \chi: T^*X \to [0,1] \end{align*}
with $\chi \in C_c^\infty(U)$ and $\chi = 1$ on an open neighbourhood of $\overline{V}$.
Because $a_m$ is elliptic on $U$, the reciprocal
\begin{align*}
a_m^{-1}: U \to \mathbb{C}
\end{align*}
belongs locally to the symbol class $S_h^{-m}(U)$. Define the initial inverse symbol
\begin{align*} b_0: T^*X \to \mathbb{C} \end{align*}
by
\begin{align*}
b_0(\rho) = \chi(\rho)a_m(\rho)^{-1}
\end{align*}
for $\rho \in U$, and extend it by $0$ outside $\operatorname{supp}\chi$. Then $b_0 \in S_h^{-m}(T^*X)$, and on a neighbourhood of $\overline{V}$ one has
\begin{align*}
b_0 a_m = 1.
\end{align*}
[/step]
[step:Construct a left inverse symbol by cancelling errors recursively]
Let $\#$ denote the semiclassical symbol product associated to the chosen quantization. By the semiclassical symbolic composition formula (citing a result not yet in the wiki: semiclassical symbolic composition formula), the product $b_0 \# a$ lies in $S_h^0(T^*X)$ and has principal term $\chi$. Hence there is a symbol
\begin{align*} r_1: T^*X \to \mathbb{C} \end{align*}
with $r_1 \in S_h^{-1}(T^*X)$ microlocally near $\overline{V}$ such that
\begin{align*}
b_0 \# a = \chi + h r_1
\end{align*}
microlocally near $\overline{V}$.
We now define symbols
\begin{align*} b_j: T^*X \to \mathbb{C} \end{align*}
with $b_j \in S_h^{-m-j}(T^*X)$ recursively. Suppose that $b_0,\dots,b_{N-1}$ have been chosen so that, with
\begin{align*}
c_{N-1} = \sum_{j=0}^{N-1} h^j b_j,
\end{align*}
one has
\begin{align*}
c_{N-1} \# a = \chi + h^N r_N
\end{align*}
microlocally near $\overline{V}$ for some $r_N \in S_h^{-N}(T^*X)$ microlocally near $\overline{V}$. On the region where $\chi=1$, define the next correction by
\begin{align*}
b_N(\rho) = -\chi(\rho)a_m(\rho)^{-1} r_N(\rho).
\end{align*}
Then $b_N \in S_h^{-m-N}(T^*X)$. The principal part of $h^N b_N \# a$ is $h^N b_N a_m$, so the choice of $b_N$ cancels the $h^N r_N$ term microlocally near $\overline{V}$. Therefore
\begin{align*}
\left(c_{N-1}+h^N b_N\right)\# a = \chi + h^{N+1}r_{N+1}
\end{align*}
microlocally near $\overline{V}$ for some $r_{N+1} \in S_h^{-N-1}(T^*X)$ microlocally near $\overline{V}$.
[guided]
The point of the recursion is to build an inverse one asymptotic order at a time. We already arranged that $b_0a_m=1$ where the parametrix is needed, so the composition $b_0 \# a$ is equal to $1$ at principal-symbol level on $V$. The remaining error begins at order $h$.
Let
\begin{align*} c_{N-1}: T^*X \to \mathbb{C} \end{align*}
be the partial symbol
\begin{align*}
c_{N-1} = \sum_{j=0}^{N-1} h^j b_j.
\end{align*}
Assume that this partial inverse has already been constructed so that
\begin{align*} c_{N-1}\# a = \chi + h^N r_N \end{align*}
microlocally near $\overline{V}$, where
\begin{align*} r_N: T^*X \to \mathbb{C} \end{align*}
belongs to $S_h^{-N}(T^*X)$ microlocally near $\overline{V}$. We want to remove exactly the visible error $h^Nr_N$.
The symbolic composition formula says that the leading contribution of $b_N \# a$ is $b_Na_m$. Thus the leading contribution of $h^N b_N \# a$ is $h^N b_Na_m$. Since $a_m$ is elliptic on $U$, and since $\chi$ is supported inside $U$ and equals $1$ near $\overline{V}$, we may divide by $a_m$ there. Define
\begin{align*} b_N: T^*X \to \mathbb{C} \end{align*}
by
\begin{align*}
b_N(\rho) = -\chi(\rho)a_m(\rho)^{-1}r_N(\rho).
\end{align*}
Because $a_m^{-1}$ has order $-m$ and $r_N$ has order $-N$, this gives $b_N \in S_h^{-m-N}(T^*X)$ microlocally near $\overline{V}$.
Now compute the new partial product:
\begin{align*}
\left(c_{N-1}+h^N b_N\right)\# a = c_{N-1}\# a + h^N b_N\# a.
\end{align*}
The first term is $\chi+h^Nr_N$ by the induction hypothesis. The principal part of the second term is $h^Nb_Na_m=-h^N\chi r_N$, which equals $-h^Nr_N$ near $\overline{V}$ because $\chi=1$ there. Hence the order-$h^N$ error cancels. All terms left over from the symbolic product have one additional power of $h$, so the new remainder has the form
\begin{align*}
h^{N+1}r_{N+1}
\end{align*}
microlocally near $\overline{V}$, with $r_{N+1}\in S_h^{-N-1}(T^*X)$ there. This completes the inductive step.
[/guided]
[/step]
[step:Borel sum the formal left inverse symbol]
The recursive construction gives a formal asymptotic series
\begin{align*}
\sum_{j=0}^{\infty} h^j b_j
\end{align*}
with $b_j \in S_h^{-m-j}(T^*X)$. By semiclassical Borel summation for symbol classes (citing a result not yet in the wiki: semiclassical Borel summation theorem), there exists a symbol
\begin{align*}
b_L: T^*X \to \mathbb{C}
\end{align*}
with $b_L \in S_h^{-m}(T^*X)$ and
\begin{align*}
b_L \sim \sum_{j=0}^{\infty} h^j b_j.
\end{align*}
For every $N \in \mathbb{N}$, the difference
\begin{align*}
b_L-\sum_{j=0}^{N-1}h^j b_j
\end{align*}
belongs to $h^N S_h^{-m-N}(T^*X)$. Combining this asymptotic property with the recursive cancellation gives
\begin{align*}
b_L \# a = \chi + r_L^\sharp
\end{align*}
microlocally near $\overline{V}$, where
\begin{align*}
r_L^\sharp \in h^\infty S_h^{-\infty}(T^*X)
\end{align*}
microlocally near $\overline{V}$.
[/step]
[step:Quantize the left inverse symbol]
Let
\begin{align*} B_L = \operatorname{Op}_h(b_L): C_c^\infty(X) \to C^\infty(X) \end{align*}
be a properly supported quantization of $b_L$. Since $b_L \in S_h^{-m}(T^*X)$, we have $B_L \in \Psi_h^{-m}(X)$. Define $S_L$ to be the smoothing remainder in the composition formula. The symbolic composition formula gives
\begin{align*} B_LA = \operatorname{Op}_h(b_L\# a) + S_L \end{align*}
with $S_L \in h^\infty\Psi_h^{-\infty}(X)$ microlocally near $\overline{V}$. Because $\chi=1$ near $\overline{V}$ and $b_L\# a=\chi+r_L^\sharp$ there, it follows that
\begin{align*}
B_LA = I + R_L
\end{align*}
microlocally on $V$, where
\begin{align*}
R_L \in h^\infty\Psi_h^{-\infty}(X)
\end{align*}
microlocally on $V$.
[/step]
[step:Construct the right inverse symbol by the same recursive argument]
The same construction, now applied to the product $a\# b_R$, gives a symbol
\begin{align*} b_R: T^*X \to \mathbb{C} \end{align*}
with $b_R \in S_h^{-m}(T^*X)$, principal term $\chi a_m^{-1}$, and
\begin{align*}
a\# b_R = \chi + r_R^\sharp
\end{align*}
microlocally near $\overline{V}$, where
\begin{align*}
r_R^\sharp \in h^\infty S_h^{-\infty}(T^*X)
\end{align*}
microlocally near $\overline{V}$. Quantizing
\begin{align*} B_R = \operatorname{Op}_h(b_R): C_c^\infty(X) \to C^\infty(X) \end{align*}
therefore gives $B_R \in \Psi_h^{-m}(X)$ and
\begin{align*}
AB_R = I + R_R
\end{align*}
microlocally on $V$, with
\begin{align*}
R_R \in h^\infty\Psi_h^{-\infty}(X)
\end{align*}
microlocally on $V$.
[/step]
[step:Use one operator for both the left and right parametrices]
It remains to arrange that the same operator gives both identities. Since $B_LA=I+R_L$ and $AB_R=I+R_R$ microlocally on $V$, we compare $B_L$ and $B_R$ on $V$:
\begin{align*}
B_L = B_L(AB_R-R_R)
\end{align*}
microlocally on $V$. Associativity of the semiclassical calculus gives
\begin{align*}
B_LAB_R = (B_LA)B_R
\end{align*}
microlocally on $V$, hence
\begin{align*}
B_LAB_R = (I+R_L)B_R = B_R + R_LB_R
\end{align*}
microlocally on $V$. Because composition of an element of $h^\infty\Psi_h^{-\infty}(X)$ with an element of $\Psi_h^{-m}(X)$ remains in $h^\infty\Psi_h^{-\infty}(X)$ microlocally on $V$, both $R_LB_R$ and $B_LR_R$ are rapidly smoothing there. Thus
\begin{align*}
B_L-B_R \in h^\infty\Psi_h^{-\infty}(X)
\end{align*}
microlocally on $V$.
Set
\begin{align*}
B = B_L.
\end{align*}
Then $BA=I+R_L$ microlocally on $V$ by construction. Also, since $B-B_R$ is rapidly smoothing microlocally on $V$ and $A\in\Psi_h^m(X)$, the composition $A(B-B_R)$ is rapidly smoothing microlocally on $V$. Define $R_R' := R_R + A(B-B_R)$ microlocally on $V$. Therefore
\begin{align*}
AB = AB_R + A(B-B_R) = I + R_R'
\end{align*}
microlocally on $V$, where $R_R' \in h^\infty\Psi_h^{-\infty}(X)$ microlocally on $V$.
Finally, the principal symbol of $B=B_L$ is the principal term of $b_L$, namely $\chi a_m^{-1}$. Since $\chi=1$ on a neighbourhood of $\overline{V}$, the principal symbol of $B$ on $V$ is $a_m^{-1}$. This proves the claimed two-sided semiclassical microlocal parametrix on $V$.
[/step]
