ladder-calculus/coq/_CoqProject

-R . LadderTypes
metatheory/AdditionalTactics.v
metatheory/ListFacts.v
metatheory/FiniteSets.v
metatheory/FSetNotin.v
metatheory/Atom.v
metatheory/Environment.v
metatheory/Metatheory.v

terms/debruijn.v
terms/equiv.v
terms/eval.v
typing/env.v
typing/subtype.v
typing/morph.v
typing/typing.v
lemmas/subst_lemmas.v
lemmas/typing_weakening.v
lemmas/typing_regular.v
lemmas/typing_inv.v
lemmas/transl_inv.v
soundness/translate_morph.v
soundness/translate_expr.v