Pruebas de equivalencia de definiciones de inversa

En Lean, está definida la función

tal que (reverse xs) es la lista obtenida invirtiendo el orden de los elementos de xs. Por ejemplo,

Su definición es

Una definición alternativa es

Demostrar que las dos definiciones son equivalentes; es decir,

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]