An illustration of coinduction in terms of a notion of weak bisimilarity is presented. First, an operational semantics $\mbox{${\cal O}$}$ for while programs is defined in terms of a final automaton. It identifies any two programs that are weakly bisimilar, and induces in a canonical manner a compositional model $\mbox{${\cal D}$}$. Next $\mbox{${\cal O}$}= \mbox{${\cal D}$}$ is proved by coinduction.