nominal-sets. Agda
equ. Chequeador de demostraciones de lógica ecuacional
universal-algebra. Formalization of Universal Algebra
yahc. yahc is a checker for derivations of propositional calculus. Its main goal is to help first year students.