@misc{indiciaedbc9d7dc3433,
  title = {A Machine-checked proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory},
  author = {William DeMeo and Jacques Carette},
  year = {2021},
  url = {https://arxiv.org/abs/2101.10166},
  note = {Source identifier: 2101.10166}
}