Agda.TypeChecking.Irrelevance
Dom
hideAndRelParams
inverseApplyRelevance
applyRelevance
Context
workOnTypes
doWorkOnTypes
workOnTypes'
applyRelevanceToContext
wakeIrrelevantVars
prop_galois
tests