Caminati, M. B. (2010). Basic first-order model theory in Mizar. Journal of Formalized Reasoning, 3(1), 49–77. https://doi.org/10.6092/issn.1972-5787/1974