Welcome to the companion proof directory for our LFMTP2014 submission "A Generic Approach to Proofs about Substitution"

This page contains quotes from the paper and hyperlink(s) to the Coq lemma(s) formalizing the claim(s) in that quote. The quotes are ordered according the the place they occur in the paper.

Section 2

Section 4

SubSection 4.1

Section 5

Paragraph : Nominal Logic
Paragraph : Alpha Equality
Paragraph : Substitution
The 5 lemmas listed in the paper correspond to the Coq lemma(s) in the following 5 lines respectively.