(* It is worth to observe that the previous algorithm works by recursion over the first
argument. This means that, for instance, (add O x) will reduce to x, as expected, but (add x O)
-is stack. How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do it
+is stuck. How can we prove that, for a generic x, (add x O) = x? The mathematical tool to 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.