1 2 3
x
| 1 2 3
x
|
| Although this proofweb is a bit more complex than our in previous examples,
the main point is that it was built using what we learned from the failures in
our previous
attempts at the same main goal, that reversing a list twice yields the
original list. This is similar to Joseph Campbell's notion of the hero's journey, a dangerous
mission where failure can nevertheless result in bringing back valuable
information or artifacts to the tribe.
It is also interesting to see how Kumo handles the associativity of append
once it has been proved, by overwriting the declaration of that operation with
a new declaration with the |