Let $S_d[\text{repeat S until b}] = FIX\ F$, where $F\ g = cond(B[b], id, g)\circ S_d[S]$ and $FIX\ F$ is the least fixed point of $F$, defined as $FIX\ F=\sqcup \{F^n \bot : n > 0\}$ ($\bot$ is the empty function).
Also let $S_d[\text{S ; while $\neg$b do S }] = FIX\ F'\circ S_d[S]$, where $F' g = cond(B[\neg b], g\circ S_d[S], id)$.
We want to show that $S_d[\text{repeat S until b}] = S_d[\text{S ; while $\neg$b do S }]$.
In order to show that, I thought I would show that $S_d[\text{S ; while $\neg$b do S }]$ is the least fixed point of $F$.
Sure enough, if we substitute into $F\ g$ we find that: $$ F\ S_d[\text{S ; while $\neg$b do S }] = cond(B[b], id, FIX\ F'\circ S_d[S])\circ S_d[S] = F'\ FIX\ F' \circ S_d[S] = FIX\ F' \circ S_d[S] = S_d[\text{S ; while $\neg$b do S }] $$
So $S_d[\text{S ; while $\neg$b do S }]$ is a fixed point of $F$.
But how can I show that it is, in fact, the least fixed point?