all.agda

open import Nat
open import Prelude

open import core-type
open import core-exp
open import core-subst
open import core

open import weakening
open import eq-dec
open import ground-dec

open import lemmas-index
open import lemmas-consistency
open import lemmas-prec
open import lemmas-meet
open import lemmas-ground
open import lemmas-ctx
open import lemmas-wf
open import lemmas-subst
open import lemmas-complete

open import typing-subst

open import elaborability
open import elaboration-generality
open import elaboration-unicity
open import typed-elaboration
open import type-assignment-unicity

open import preservation
open import progress 

open import complete-elaboration
open import complete-preservation
open import complete-progress

open import parametricity
open import graduality

module all where