ForMatUS: Eliminación de la disyunción en Lean

En el vídeo se comentan distintas demostraciones sobre la eliminación de la disyunción en Lean: con tácticas, con término de prueba y 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