This question is a follow up to my previous question on rings of crystaline differential operators, to which I refer for the adequate definitions.
First, let's consider the case of an algebraically closed field of zero characteristic $\mathsf{k}$ and usual rings of differential operators (denoted here by $\mathcal{D}(\cdot)$) All varieties are irreducible.
Let $X$ be an affine smooth variety and $A=\mathcal{O}(X)$ its ring of regular functions. $\mathcal{D}(X)$ and $\mathcal{D}(A)$ mean the samething.
One of the most useful basic facts about rings of differential operators, and which allows us to sheafify, is following:
Proposition 1: Let $S$ be a multiplicatively closed subset of $A$. Then left and right localization of $\mathcal{D}(A)$ by $S$ exists and $\mathcal{D}(A)S^{-1}=S^{-1}\mathcal{D}(A)=\mathcal{D}(AS^{-1})$.
The next result I am going to recall is much more deep. It usually is treated as a folklore, and hence I am not sure about who was the first one to prove it, but its proof appears in print only in a paper of Cannings and Holland.
Theorem 1: Let $G$ be a finite group acting freely on a smooth affine variety $X$. Then $\mathcal{D}(X)^G \simeq \mathcal{D}(X/G)$.
Now we move to crystaline rings of differential operators. Now $\mathsf{k}$ has prime characteristic, and I denote the ring of crystalline differential operators by $\mathcal{D}_c(\cdot)$.
I was reading the following paper by Tikaradze, and in the proof of Lemma 0.2 it seems to me that he uses implictly the following 'crystalline' analogues of the above proposition and theorem:
Proposition 1*: Let $X$ and $Y$ be two smooth affine varieties such that the function fields $\mathsf{k}(X)$ and $\mathcal{k}(Y)$ are isomorphic. Then $\operatorname{Frac}(\mathcal{D}_c(X)) \simeq \operatorname{Frac}(\mathcal{D}_c(Y))$, where $\operatorname{Frac}$ denotes the skew field of fractions an Ore domain.
Theorem 1*: Let $X$ be an smooth affine variety and $G$ a finite group acting freely on it. Then $\mathcal{D}_c(X)^G \simeq \mathcal{D}_c(X/G)$.
The main reference I know of about rings of crystalline differential operators is Roman Bezrukavnikov, Ivan Mirković, Dmitriy Rumynin: "Localization of modules for a semisimple Lie algebra in prime characteristic". In this paper the authors shows that $\mathcal{D}_c(\cdot)$ sheafifies, and hence I think that the above Proposition 1* is more or less a direct consequence of this. I am correct, or should I look for a proof for Proposition 1*?
Things are different in regarding Theorem 1*. It definitely does not follow form what is done in the paper by Bezrukavnikov, Mirković and Rumynin. Hence I am looking for a proof of this fact - I couldn't find any.
Justification for this question: I am writing a short paper where I pretend to use Proposition 1* and Theorem 1*, and I would like to include adequate proofs/references for these statements.