This project was built with coq version 8.7.2.

This project uses Autosubst (https://github.com/uds-psl/autosubst). It must be installed from the coq86-devel branch as described in the README of Autosubst.

For inversion the inverts ... as tactic from lib/LibTactics.v is used.

Naming convention:
GQM-Formulas: A,B,C..., sometimes f,g,...
Context: c

To build the project run
$ make

There are several ways to build a documentation.
- HTML with proofs:     $ make html
- HTML without proofs:  $ make gallinahtml
- pdf with proofs:      $ make all.pdf
- pdf without proofs:   $ make all-gal.pdf
HTML documentation can be found in the html subfolder, pdf documentation is created in the main folder as all.pdf or all-gal.pdf.