The artifact reviewers have three options: 1) They can checkout the git repo dedicated to the Coq proof. In its README.md file, one can find the following: The requirements to compile the Coq code How one can install these requirements Documentation explaining where one can find the relevant definitions and proofs with references to the paper. 2) They can download the virtualbox compatible VM file to interact with the artifact. It contains a copy of the aforementioned git repo (/home/username/fae-gtlc-mu), and it has the required version of Coq and the necessary libraries preinstalled. The VM also contains CoqIDE (linked on the dekstop), a gui to interact with the Coq code. The Coq files are already compiled; to recompile from scratch, one can do successively run 'make clean' and 'make' in the directory. 3) They can download a zip file that contains a collection of clickable html files generated by coqdoc. One can start by looking at the overview.html file; it provides the same documentation as the README.md file of the aforementioned git repository.