Binary intersection formalized

The purpose of this article is twofold. First, we reformulate here the result in terms of morphisms which allows an exposition that is much shorter, and hopefully also more transparent. This layer of the article is a slightly modified version of [2]. Second, we complement the improved "human" proof with a formalization in the proof assistant Isabelle/HOL. It is well known that an intersection of two free submonoids of a free monoid is free.