Import "olist".
Import "nat".
Import "rules".
Import "declarative".
Import "order".
Import "alg".
Import "trans".
Import "nonOverlap".
Import "substwl".
Import "soundness".
Import "depth".
Import "dcl".
Import "completeness".
Import "decidability".
Import "smallStep".
Import "safety".
/*
| Paper | File | Name in Abella |
|----------------|-------------------------------------|--------------------------------------------------------------|
| Theorem 3.1 | `declarative.thm` | `Theorem sub_refl` |
| Theorem 3.2 | `nonOverlap.thm` | `Theorem sub_trans` |
| Theorem 3.3 | `nonOverlap.thm` | `Theorem chk_subsumption` |
| Lemma 3.4 | `nonOverlap.thm` | `Theorem sub_narrow_sty`, `Theorem sub_subst` |
| Lemma 3.5 | `nonOverlap.thm` | `Theorem infAbs_sub`, `Theorem infTApp_sub` |
| Lemma 3.6 | `nonOverlap.thm` | `Theorem subsumption_thm` |
| Theorem 3.7 | `safety.thm` | `Theorem typ_sound_f` |
| Theorem 3.8 | `safety.thm` | `Theorem typ_complete_fsub` |
| Theorem 4.1 | `dcl.thm` | `Theorem dcl_sound`, `Theorem dcl_complete` |
| Theorem 4.2 | `soundness.thm` | `Theorem soundness` |
| Theorem 4.3 | `completeness.thm` | `Theorem completeness` |
| Lemma 4.4 | `soundness.thm`, `completeness.thm` | `Theorem tex_substwl`, `Theorem tex_substwl_inv_l` |
| Lemma 4.5 | `depth.thm` | `Theorem prune_tex_instL` |
| Theorem 4.6 | `smallStep.thm` | `Theorem reduction_det` |
| Corollary 4.7 | `smallStep.thm` | `Theorem confluence` |
| Lemma 4.8 | `decidability.thm` | `Theorem iso_equiv_nSplitTyp`, `Theorem iso_equiv_nAllTyp` |
| Lemma 4.9 | `decidability.thm` | `Theorem isoa_equiv_nSplitTyp`, `Theorem isoa_equiv_nAllTyp` |
| Lemma 4.10 | `dcl.thm` | `Theorem dcl_weaken` |
| Lemma 4.11 | `completeness.thm` | `Theorem judge_weaken` |
| Theorem 4.12 | `decidability.thm` | `Theorem decidablity` |
| Corollary 4.13 | `decidability.thm` | `Theorem decidablity_decl` |
*/
