In Arora and Barak's book "Computational Complexity: A Modern Approach" (see draft pdf here https://theory.cs.princeton.edu/complexity/book.pdf), the $\mathtt{PATH}$ problem is given as the language of triples $\langle G,s,t\rangle$ such that in digraph $G$ vertex $s$ can reach vertex $t$.
In theorem 4.16 it is stated that $\mathtt{PATH}$ is $\mathsf{NL}$-complete. This is proven using a configuration graph technique.
Then, they cite the Immerman-Szelepscényi theorem (theorem 4.18) in the form which states that $\overline{\mathtt{PATH}} \in \mathsf{NL}$.
The proof is then given using the certificate definition of $\mathsf{NL}$ whereby a language $L \in \mathsf{NL}$ if there exists a dTM $M$ with special read-once input tape polynomial $p: \mathbb{N} \to \mathbb{N}$ such that $\forall x \in \{0,1\}^*$, $$x\in L \iff \exists u \in \{0,1\}^{p(|x|)} \text{ s.t. } M(x,u)=1$$ here denoting $M$ as the 'verifier' and $u$ as the 'certificate' on the special read-once tape, and $M$ uses $\leq O(\log |x|)$ space on its read/write tapes for an input $x$.
Then to prove this theorem the approach taken is that it is sufficient to show that there exists polynomial certificate $u$ such that the verifier $A$ outputs $A(\langle G,s,t\rangle,u =1$ iff there is no path from $s$ to $t$ (unreachable).
Using configuration graphs the corollary (4.19) is furthermore reached that for every space constructible $S(n) > \log n$, $\mathsf{NSPACE}(S(n)) = \mathsf{coNSPACE}(S(n))$.
What I am unsure of is whether $\mathsf{coNL} = \mathsf{NL}$ follows from this as specifically $\mathsf{NL} = \mathsf{NSPACE}(\log n)$. So, should corollary 4.19 be a strict greater than for $S(n) > \log n$ or is it rather that using this particular proof technique by the authors, it only proves in the greater than case and not the case of $S(n) = \log n$?
Edit: is it because of $\overline{\mathtt{PATH}} \in \mathsf{NL}$ implying $\mathtt{PATH} \in \mathsf{coNL}$ together with $\mathtt{PATH} \in \mathsf{NL}\text{-complete}$ which implies $\mathsf{coNL} = \mathsf{NL}$ as for $A \in \mathtt{PATH}$, $B \in \mathsf{NL}$, log-reduction exists $B \leq_l A$ reducing to an instance of $\mathtt{PATH}$ which is therefore also in $\mathsf{coNL}$?
