Theorem 4.2.5 of Duistermaat's "Fourier Integral Operators", 1996, states:
Let $A \in I^m(X,Y,C)$ be an elliptic Fourier Integral Operator of order $m$, associated to a bijective canonical homogeneous transformation $C$ from an open cone $\Gamma \subset T^\ast Y \setminus 0$ into $T^\ast X \setminus 0$. Then for any closed (in $T^\ast Y \setminus 0$) cone $\Gamma_0 \subset \Gamma$ such that $C(\Gamma_0)$ is closed in $T^\ast X \setminus 0$ one can find a properly supported Fourier Integral Operator $B \in I^{-m}(Y,X,C^{-1})$ such that for any $u \in \mathscr E'(Y)$, for any $v \in \mathscr E'(X)$ the following relations are valid: $$ WF(BAu - u) \cap \Gamma_0 = \varnothing,\quad WF(ABv - v) \cap C(\Gamma_0) = \varnothing. $$
The proof of the theorem involves multiplications by smooth functions with compact supports. This is why I can't directly generalize the proof of the abovementioned theorem to the case of the real-analytic category (the only real analytic function with compact support is zero). On the other hand, I think that the theorem is still valid for real-analytic Fourier Integral Operators and for analytic wavefronts but uses some more subtle proof. Please tell me, if you have encountered the mentioned theorem (or some variants) in the real-analytic case in some paper.
