ForMatUS: Regla de eliminación del condicional en Lean

He añadido a la lista Lógica con Lean el vídeo Regla de eliminación del condicional en Lean en el que se comentan 7 demostraciones en Lean de la regla de eliminación del condicional en distintos estilos (declarativo, aplicativo con tácticas, funcional con término de prueba y automático). Además,se presenta el entorno de trabajo de Lean en la Red (que permite hacer las pruebas en el navegador sin necesitar ninguna instalación).

Los enlaces correspondientes son:

A continuación, se muestra el vídeo