%% Preliminaries

base/nat.elf
base/nat.thm
base/pre-syntax.elf

%% Singleton metatheory

sing/constant.elf
sing/il.elf
sing/ile.elf
sing/il-simp.elf
sing/expand.elf
sing/subtype.elf
sing/el.elf
sing/algorithm.elf
sing/translate.elf
sing/convert.elf
sing/equality.thm
sing/subst-fun.thm
sing/strengthen.thm
sing/explicit-lemmas.thm
sing/regularity.thm
sing/subst-effect.thm
sing/inversion.thm
sing/substitution.thm
sing/expand.thm
sing/subtype-lemmas.thm
sing/trans-fun.thm
sing/trans-reg.thm
sing/trans-sub.thm
sing/esubstitution.thm
sing/functionality.thm
sing/eregularity.thm
sing/convert-effect.thm
sing/convert-explicit.thm
sing/convert-reg-il.thm
sing/convert-fun.thm
sing/convert-normal.thm
sing/convert-sub.thm
sing/convert-reg.thm
sing/sound.thm
sing/complete.thm
sing/flay.thm
sing/correct.thm
sing/el-inversion.thm

%% Internal language

il/syntax.elf
il/value.elf
il/static.elf
il/opsem.elf
il/singleton.elf

%% Type safety

safety/equality.thm
safety/functionality.thm
safety/regularity.thm
safety/flay-il.thm
safety/substitution.thm
safety/inversion-static.thm
safety/singleton.thm
safety/principal.thm
safety/consistency.thm
safety/canon.thm
safety/inversion.thm
safety/progress.thm
safety/preservation.thm
safety/determinism.thm

%% Elaboration

elaborate/el.elf
elaborate/prepass.elf
elaborate/elaboration.elf
elaborate/resolve.elf
elaborate/ty-elab.elf
elaborate/instance.elf
elaborate/distribute.elf
elaborate/expr-elab.elf
elaborate/match-elab.elf
elaborate/pat-elab.elf
elaborate/dec-elab.elf
elaborate/strexp-elab.elf
elaborate/spec-elab.elf
elaborate/sigexp-elab.elf

%% Static correctness

correct/resolve.thm
correct/ty-elab.thm
correct/instance.thm
correct/distribute.thm
correct/elaboration.thm
correct/expr-elab.thm
correct/match-elab.thm
correct/pat-elab.thm
correct/dec-elab.thm
correct/strexp-elab.thm
correct/spec-elab.thm
correct/sigexp-elab.thm
correct/denouement.thm