ForMatUS: Regla de introducción del condicional en Lean

He añadido a la lista Lógica con Lean el vídeo Regla de introducción del condicional en Lean en el que se comentan 13 demostraciones en Lean de la regla de introducció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 el de VS Code.

Los enlaces correspondientes son:

A continuación, se muestra el vídeo