Se ha añadido el ejercicio Demostraciones con Lean4 e Isabelle/HOL de "(s \ t) ∪ t = s ∪ t", propuesto originalmente el 27 de mayo de 2021.