Overview

The proof is divided into the following files:

Running Coq

Running the Coq proofs requires the following dependencies installed using the specified versions of their opam packages:

coq 8.11.2
ott 0.31
coq-ott 0.31

It also requires lngen, installed as follows: 1) Install stack: https://docs.haskellstack.org/en/stable/ 2) Build lngen from source: git clone https://github.com/plclub/lngen.git cd lngen stack setup stack install

It also requires metalib, installed following the instructions at: https://github.com/plclub/metalib

With the above dependencies, the following commands build the proofs.