Understanding application of the internal language of a category (Elephant, D1.3.12) While studying the internal language of categories I came across the following result on Johnstone's Elephant (pag. 838, D1.3.12):

(he deliberately denotes by $f$ the corresponding function symbol $\ulcorner f \urcorner$). The cover part it is rather easy as
$$\top\vdash_x\exists y\phi\mbox{ holds iff } [[x.\top]]\leq[[x.\exists y\phi]]$$ 
and $[[x.\exists y\phi]]$ is exactly the image of $a:[[x,y.\phi]]\rightarrowtail A\times B \rightarrow A$, where $x:A$ and $y:B$: but being $[[x.\top]]\cong A$ this implies that $a$ is a cover (i.e. epi on an image)
For $a$ being monic I thought about using a previous result, stating that for regular categories $a$ is monic iff $ (\ulcorner a\urcorner (t)=\ulcorner a\urcorner(t'))\vdash_{t,t'}(t=t')$, but I couldn't manage to deduce this sequent from the one above.
Another attempt was to explicitate the sequent above in the model, but I have no idea how to express in a useful way the two subobjects $[[x,y,y'.\phi]]$ and $[[x,y,y'.\phi(y'/y)]]$. Can they be deduced from $[[x,y.\phi]]$? (perhaps as pullbacks along projections?)
So, as intuitively true as it seems, I can't find a way to prove $a$ monic: how could it be done?
 A: Letting $\langle a,b\rangle : [\![x,y.\varphi]\!]\rightarrowtail A\times B$, we have the pullback square $$\require{AMScd}
\begin{CD}
[\![x,y,y'.\varphi\land\varphi[y'/y]]\!] @>q>> [\![x,y.\varphi]\!]\times B \\
@VpVV @VV(id\times\sigma)\,\circ\,\alpha\,\circ\,(\langle a,b\rangle\times id)V \\
[\![x,y.\varphi]\!]\times B @>>\alpha\,\circ\,(\langle a,b\rangle\times id)> A\times (B\times B)
\end{CD}$$
We also have $$\begin{CD}
[\![x,y,y'.\varphi\land\varphi[y'/y]]\!] @= [\![x,y,y'.\varphi\land\varphi[y'/y]]\!] \\
@V\langle h,k\rangle VV @VVV \\
A\times B @>>id\times\langle id,id\rangle> A\times(B\times B)
\end{CD}$$ where $\langle h,k\rangle$ witnesses the fact that the subobject $[\![x,y,y'.\varphi\land\varphi[y'/y]]\!]$ factors through $id\times\langle id,id\rangle$, i.e. $\varphi(y)\land\varphi(y')\vdash_{x,y,y'}y=y'$.
Let's say we have $r,s:X\to[\![x,y.\varphi]\!]$ such that $a\circ r = a \circ s$. We want to show that this means $b\circ r = b\circ s$ at which point we'll have $\langle a,b\rangle\circ r = \langle a,b\rangle\circ s$ which implies that $r = s$ since $\langle a,b\rangle$ is a mono.
Consider the arrow $\langle r,b\circ s\rangle:X\to[\![x,y.\varphi]\!]\times B$, we have $$\begin{align}
\alpha\circ(\langle a,b\rangle\times id)\circ\langle r,b\circ s\rangle & = \alpha\circ\langle\langle a,b\rangle\circ r,b\circ s\rangle \\
& = \alpha\circ\langle \langle a\circ r, b\circ r\rangle, b\circ s\rangle \\
& = \langle a\circ r, \langle b\circ r, b\circ s\rangle\rangle
\end{align}$$
and the arrow $\langle s,b\circ r\rangle:X\to[\![x,y.\varphi]\!]\times B$ for which we have $$\begin{align}
(id\times\sigma)\circ\alpha\circ(\langle a,b\rangle\times id)\circ\langle s,b\circ r\rangle & = (id\times\sigma)\circ\alpha\circ\langle\langle a,b\rangle\circ s,b\circ r\rangle \\
& = (id\times\sigma)\circ\alpha\circ\langle\langle a\circ s, b\circ s\rangle, b\circ r\rangle \\
& = (id\times\sigma)\circ\langle a\circ s, \langle b\circ s, b\circ r\rangle\rangle \\
& = \langle a\circ s, \langle b\circ r, b\circ s\rangle\rangle
\end{align}$$
and since $a\circ r = a\circ s$ these two arrows are equal, so there is a unique arrow $t:X\to[\![x,y,y'.\varphi\land\varphi[y'/y]]\!]$ determined by them. But, $$\langle a\circ r,\langle b\circ r,b\circ s\rangle\rangle = \langle h,\langle k,k\rangle\rangle\circ t = \langle h\circ t,\langle k\circ t,k\circ t\rangle\rangle$$ so $b\circ r = k \circ t = b \circ s$.
