Assume $B_t$ is a standard real brownian motion defined on $\{\Omega,\mathcal{F},P\}$ and $X_t(y)$ satisfies the following SDE:
\begin{equation} dX_t=-\cot X_tdt+dB_t \text{ with }X_0=y \end{equation}
We know that the solution exists up to time $T(y):=\inf\{t;\sin X_t(y)=0\}$. Now fix $x\in\mathbb{R}$, define $Z_t:=X_{t\wedge T(x)}(x)$ and \begin{equation} Y_t:=P\{X_{T(Z_t)}(Z_t)=\pi\} \end{equation}
Where $X_{T(y)}(y):=\lim_{t\uparrow T(y)}X_t(y)$.
How can I prove that $Y_t$ is a martingale?
I was reading some notes about SDEs where I found this claim.