module Adequacy where

{- Adequacy of the well scoped locally nameless representation with
repect to nameful terms modulo alpha-equivalence (including
correctness for capture-avoiding substitution). -}

open import Adequacy.Nameful public
open import Adequacy.Translation public
open import Adequacy.Substitution public