ForMatUS: Formulación equivalente de lemas con dos hipótesis

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo Formulación equivalente de lemas con dos hipótesis en el que se comentan 5 demostraciones en Lean de la fórmula

(P ∧ Q → R) ↔ (P → (Q → R))

usando distintos estilos de prueba,

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