Coercion
data Coercion
type CoercionN
type CoercionR
type CoercionP
data UnivCoProvenance
data CoercionHole
data LeftOrRight
data Var
type CoVar
type TyCoVar
data Role
type NormaliseStepper ev
data NormaliseStepResult ev
type CvSubstEnv
type LiftCoEnv
data LiftingContext