In this part we collect some basic definitions and technical lemmas that are used throughout the rest of the formalisation.

{-# OPTIONS --guardedness --sized-types #-}

module Preliminaries.index where

import Preliminaries.Algebra
import Preliminaries.Base
import Preliminaries.Equivalence
import Preliminaries.List
import Preliminaries.Vector

References