[Improved comment.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080307012110] hunk ./MultiComposition.agda 162
--- unless the two sides can be unified. This is the reason for
--- formulating the lemma in this way.)
+-- unless the two sides of the equality can be unified. This is the
+-- reason for formulating the lemma in this way.)