ForMatUS: Eliminación de la equivalencia en Lean
En el vídeo se comentan distintas demostraciones sobre la eliminación de la equivalencia en Lean. La primera es con la táctica intro y las siguientes son simplificaciones de la primera hasta llegar al término de la prueba. A continuación, se presentan demostraciones estructuradas con razonamiento hacia adelante y, finalmente, se presentan demostraciones automáticas
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo