Trivial C¹ holonomy gives a saturated product neighbourhood

(Compact injectivity.) For completeness, let $G:L\times I\to M$ be a local diffeomorphism with $G(p,0)=p$, and choose a closed interval $[-e,e]\subset I$. If no smaller interval gives injectivity, the closures of its distinct equal-image pairs in the compact space $(L\times [-e,e]{)}^2$, restricted to parameters of absolute value at most $1\mathrm{/}n$, form nested nonempty closed sets. F5 gives a common point. Continuity and F6 force its parameters to be zero and its two base points to coincide. A local inverse neighborhood at that central point contains no distinct equal-image pair, contradicting membership in the closure. Thus such a map is injective on a smaller interval about zero.

(Normalized chart first integrals.) Fix a transversal $T$ at $x\in L$ with positive coordinate $t$ vanishing at $x$. Choose finitely many connected plaque neighborhoods $B_i\subseteq L$ in foliation charts with positive transverse coordinate $t_i$ and $L$ given there by $t_i=0$, and smaller relatively open $A_i$ covering $L$ with $\overline{A_i}\subseteq B_i$. Each closure is compact. Choose one point $x_i\in B_i$ and one leafwise path from $x$ to $x_i$. Its finite chart chain gives an actual positive $C^1$ transverse-coordinate diffeomorphism $h_i$ near zero, from the coordinate on $T$ to $t_i$. On a neighborhood of $\overline{A_i}$ define the $C^1$ first integral $r_i=h_i^{-1}\circ t_i$, shrinking its domain so the inverse is defined. For any $p\in B_i$, continuing that path inside the connected plaque $B_i$ identifies the same label $r_i$ with the starting coordinate $t$.

(A transverse collar.) Consider all pairs consisting of a smooth ambient coordinate vector, positively transverse to the continuous tangent hyperplanes of $L$ on its coordinate neighborhood, and a nonnegative chart bump supported there. Such vectors exist locally by continuity, and the positive sets of the bumps from F7 cover $L$. Retain finitely many and sum the corresponding nonnegative bump multiples of the vectors, extending each summand by zero. The resulting smooth field $V$ is positively transverse along $L$. Its flow gives a $C^1$ map $C(p,s)={\mathrm{Fl}}_s^V(p)$ on $L\times (-a,a)$ for some $a>0$ by compactness. At $(p,0)$ its derivative is $(v,b)\mapsto v+b{V}_p$, hence invertible by F3. After shortening $a$, $C$ is a local diffeomorphism everywhere and injective: the compact bad-pair argument in step 1.1 applies to any such map equal to the inclusion at $s=0$. Thus $C$ is a $C^1$ collar; write $P(C(p,s))=p$ for its $C^1$ projection. The finite bump selection uses compactness, not a partition of unity on an arbitrary cover or an additional choice axiom.

(Equality on actual overlaps.) If $p\in B_i\cap B_j$, the two paths from $x$ to $p$ just described differ by a loop in $L$. Its transport germ is the identity by F1. Hence $r_i$ and $r_j$ agree as transverse-coordinate germs on the collar fibre through $p$. Locally both are functions of one foliation-chart transverse coordinate, whose restriction to that fibre is a local diffeomorphism; equality on a small fibre interval therefore implies equality on an ambient neighborhood of $p$. The compact set $K_{ij}=\overline{A_i}\cap \overline{A_j}\subseteq B_i\cap B_j$ has a neighborhood on which these actual functions agree. There are finitely many pairs. Compactness in the collar gives one $b>0$ such that each $r_i$ is defined on $C(\overline{A_i}\times [-b,b])$ and every such pair agrees on $C(K_{ij}\times [-b,b])$. The functions thus glue on the open collar $C(L\times (-b,b))$ to a $C^1$ function $r$ constant on local plaques, with $r(p)=0$ on $L$ and ${\mathrm{\partial }}_s(r\circ C)(p,0)>0$. This is a finite compact-overlap argument; it imposes no simultaneous equality on an arbitrary family of path representatives.

(The product map.) Shorten $b$ so that ${\mathrm{\partial }}_s(r\circ C)>0$ on $L\times [-b,b]$. The endpoint values at $s=-b$ are negative and those at $s=b$ positive, uniformly away from zero by compactness. Choose $d>0$ smaller than both absolute endpoint bounds and set $D_0=(-d,d)$. For each $(p,t)\in L\times D_0$, the intermediate value theorem and strict monotonicity give a unique $s\in (-b,b)$ with $r(C(p,s))=t$. The map $(p,s)\mapsto (p,r(C(p,s)))$ has invertible derivative, so its inverse is $C^1$ by F3. Composing with $C$ yields $\mathrm{\Phi }:L\times D_0\to M$, with $P(\mathrm{\Phi }(p,t))=p$, $r(\mathrm{\Phi }(p,t))=t$ and $\mathrm{\Phi }(p,0)=p$. It is a local diffeomorphism and carries every connected slice into one leaf, because the level sets of $r$ are locally precisely plaques. This includes point leaves when $\dim M=1$.

(Saturation.) The identities $P(\mathrm{\Phi }(p,t))=p$ and $r(\mathrm{\Phi }(p,t))=t$ make $\mathrm{\Phi }$ injective; take $D=D_0$. Its image $U$ is open. A slice image is nonempty, compact, connected and open in its intrinsic leaf topology; the intrinsic inclusion is continuous by its local plaque expressions. That leaf is Hausdorff, so this compact image is also closed there and therefore is the whole connected leaf. Hence $U$ is saturated, and the injective local diffeomorphism $\mathrm{\Phi }$ is a foliated $C^1$ diffeomorphism onto $U$.

Thus $(U,F{\mathrm{\mid }}_U)\cong (L\times D,\{L\times \{t\}\})$ is the required saturated $C^1$ product neighborhood. Only finitely many chart, path and bump choices were used.