ForMatUS: Conmutatividad de la conjunción en Lean

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo Conmutatividad de la conjunción en Lean en el que se comentan 9 demostraciones en Lean de la conmutatividad de la conjunción usando los distintos estilos: aplicativa con táctica, declarativa estructurada, funcional con término de prueba y automática.

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