Text this: Formalização da prova do teorema de existência de unificadores mais gerais em teorias de primeira-ordem