ForMatUS: Reglas de la conjunción en Lean

He añadido a la lista Lógica con Lean el vídeo Reglas de la conjunción en Lean en el que se e comentan 10 demostraciones en Lean que usan las reglas de introducción y eliminación de la conjunción en distintos estilos (declarativo, aplicativo con tácticas, funcional con término de prueba y automático).

Los enlaces correspondientes son:

A continuación, se muestra el vídeo