ForMatUS: Pruebas en Lean de ∃x∃y P(x,y) ↔ ∃y∃x P(x,y)

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de la propiedad

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada