module Implicit.Algo.All where

open import Implicit.Algo.Base public
open import Implicit.Algo.Properties.Shift public

open import Implicit.Algo.Properties.Weaken public

open import Implicit.Algo.Properties.Id public
open import Implicit.Algo.Properties.Subst public
open import Implicit.Algo.Properties.Polarity public

open import Implicit.Algo.Properties.Extension public
open import Implicit.Algo.Properties.Regularity public

open import Implicit.Algo.Properties.Irrelevance public
open import Implicit.Algo.Properties.Subsumption public
open import Implicit.Algo.Properties.OpenK public
open import Implicit.Algo.Properties.SubIrrelevance public