module NCILL.Ctx where

open import Data.List

open import NCILL.Types

-- CONTEXT
------------------------------------------------------------------------

-- Context is a _list_ without. Not a set or multiset.
-- That makes proving very direct.
Ctx = List Ty