¹In the semantics for addition as we wrote them, the left-hand side was a, which referred to numbers, rather than any irreducible expression, but we would run into a similar problem no matter how we implement +. Note also that we used + as a shorthand for list concatenation, but that was a shorthand for the premises, and not part of our language.