ForMatUS: Introducción de la implicación en Lean
En el vídeo se comentan distintas demostraciones sobre la introducción de la implicación 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. 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