Coq files and Documentation
This proof is decomposed in a number of modules, dealing with
different aspects.

tools
(link)This
module contains simple notations, definitions, tactics and
lemmas, mostly independant of the rest of the developpement.

atoms
(link)Here we
simply define atoms, and permutations of atoms.

atoms_ops
(link)This
library defines a number of operations on lists of atoms.

equiv_lst
(link)Defines
an equivalence relation on lists of atoms.

letter
(link)Introduces
letters.

expr
(link)The type
of expressions is defined, together with some elementary
functions such as size, equality...

predicates
(link)We
define in this library some predicates over expressions,
such as typing, freshness...

morphisms
(link)The
important functions manipulating expressions can be found
here.

proofs
(link)In
this library the generic proof system is defined, as well as
the various axiom bundles.

rm0
(link)The
technical proofs dealing with bridges between positive and
nonpositive theories.

removetype
(link)The
technical proofs dealing with bridges between typed and
untyped theories.

perm
(link)The
technical proofs dealing with bridges between theories with
our without explicit permutations.

theories
(link)Definition
of the different theories, and stability results about them.

sg_to_mlt
(link)The
technical proofs dealing with bridges from atomic to
literate theories.

order
(link)Definitions
of the preorder relations on theories, and proofs of the
ordering of our theories.
restr_atoms,normalise
(link1,
link2)
The other files are still in a preliminary state.