Text this: Uma formalização da teoria nominal em Coq