Trakhtenbrot in Coq, IJCAR 2020 selected papers (LMCS) v1.0

This release is tailored version of the Coq Library of Undecidability Proofs focusing on the TRAKHTENBROT development and in sync with the submission of an extended version for the selected papers of IJCAR 2020 paper, submitted to LMCS via Arxiv:

Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens by Dominik Kirst and Dominique Larchey-Wendling

An overview file called summary.v is provided which links the results list in the submission with source code references. Please consult the README.md file for compilations instructions.