{-# OPTIONS --without-K #-} module README where import Everything open import Context open import Parameters as _ using (Parameters) import IK x = nf {· , ι} (app (abs (var zero)) (var zero)) where open import Calculus record { IK } -- Instantiate the calculus IK -- Show soundness and completeness of normalization for all parametrizations module _ (params : Parameters) where open import Soundness params open import Completeness params