Agda.TypeChecking.Monad.Closure
enterClosure
withClosure
mapClosure