The normal model map restricts to a diffeomorphism onto a saturated neighbourhood

(Injectivity on a small model.) The central leaf $\mathrm{\Sigma }$ maps injectively onto $L$ and $\bar{\mathrm{\Phi }}$ is a local diffeomorphism there [F1]. The finite cover $\widehat{L}$ is compact [F4]. Use the linearized transverse coordinates specified in F2. Average a Euclidean inner product over the finite derivative representation of $H$; every group element preserves its norm. Choose a closed ball inside the linearized image of $D$, and smaller radii $r_n\to 0$. Pulling those balls back through the conjugating coordinate gives nested invariant compact disks $K_n\subseteq D$, with intersection $\{x\}$. Their interiors are disk-like without a further exponential-map prerequisite. Then $Q_n:=(\widehat{L}\times K_n)\mathrm{/}H$ is compact by F5, and ${\bigcap }_n{Q}_n=\mathrm{\Sigma }$: the orbit-invariant distance to $x$ tends to zero precisely on the central slice. Put $C_n:=\{(u,v)\in Q_n^2:\bar{\mathrm{\Phi }}(u)=\bar{\mathrm{\Phi }}(v)\}$ and let $E_n$ be the closure in $Q_1^2$ of $C_n\setminus \mathrm{\Delta }$. Each $C_n$ is closed by F6. If no sufficiently small open model is injective, every $E_n$ is nonempty; these are nested compact closed sets, so F5 supplies $z\in {\bigcap }_n{E}_n$. Since $E_n\subseteq C_n$, both components of $z$ lie in $\mathrm{\Sigma }$ and have the same image, hence $z=(u,u)$ by central injectivity. A local inverse neighborhood $V$ of $u$ contains no distinct pair with equal image, whereas $z\in E_1$ requires every neighborhood of $z$ to meet $C_1\setminus \mathrm{\Delta }$. The contradiction yields an invariant open disk-like ball $D^{\mathrm{\prime }}\subseteq D$ on whose model $\bar{\mathrm{\Phi }}$ is injective. This works in every transverse dimension; in dimension zero $D=\{x\}$ and central injectivity already suffices. No bad-pair sequence or choice principle is used.

(Diffeomorphism onto a saturated neighbourhood.) The image $U$ is open, and injectivity makes $\bar{\mathrm{\Phi }}$ a diffeomorphism onto $U$ [F3]. Each model leaf is $\widehat{L}\mathrm{/}{H}_t$ for a finite stabilizer $H_t$, hence compact by F2 and F4. Its image lies in one ambient leaf and is open in that leaf by the foliated local inverse charts [F1]; it is also closed in that leaf, since the map into its intrinsic Hausdorff topology is continuous in plaque charts and has compact domain. The image is nonempty, so connectedness of the ambient leaf makes it the whole leaf. Thus $U$ is a union of complete ambient leaves and is saturated. It contains $L$ by the central identification. For a prescribed open neighborhood $W$ of $L$, the preimage of $W$ under $\mathrm{\Phi }$ is open and contains $\widehat{L}\times \{x\}$; a finite product-chart cover of compact $\widehat{L}$ gives a common transverse neighborhood contained in that preimage. A smaller invariant ball $D^{\mathrm{\prime }}$ therefore makes $U\subseteq W$.

(Leaves of the image.) Every leaf of $F{\mathrm{\mid }}_U$ is the image of a model leaf $\widehat{L}\times \{t\}$ modulo its finite stabilizer $H_t$ [F1, F2]; since $H$ is finite and $L$ is compact, $\widehat{L}$ is compact (it finitely covers $L$) and each such leaf is compact, is finitely covered by $\widehat{L}$, and has finite holonomy group $H_t$ [F2]. This proves the leaf description of the model neighbourhood.