-(* It is worth to observe that the previous algorithm works by recursion over the
-first argument. This means that, for instance, (add 0 x) will reduce to x, as expected,
-but (add x 0) is stack. How can we prove that, for a generic x, (add x 0) = x? The
-mathematical tool do it is called induction. The induction principle states that,
-given a property P(n) over natural numbers, if we prove P(0) and prove that, for any
-m, P(m) implies P(S m), than we can conclude P(n) for any n.
+(* It is worth to observe that the previous algorithm works by recursion over the first
+argument. This means that, for instance, (add 0 x) will reduce to x, as expected, but (add x 0)
+is stack. How can we prove that, for a generic x, (add x 0) = x? The mathematical tool do it is
+called induction. The induction principle states that, given a property P(n) over natural
+numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m), than we can conclude
+P(n) for any n.