Получение значения, которое должно было быть удалено во время выполнения

Рассмотрим следующее определение зависимого типа данных:

data Container : Nat -> Type where
   Level : {n : _} -> Container n

Следующая функция компилируется:

getLevel : Container n -> Nat
getLevel Level = n

Однако, если я укажу нулевую кратность вместо неограниченной для n в Level:

data Container : Nat -> Type where
   Level : { 0 n : _ } -> Container n
            ^^^

Тогда функция getLevel больше не компилируется:

Ошибка: при обработке правой части getLevel. n недоступен в этом контексте.

Для меня это имеет смысл, поскольку нулевая кратность означает, что n стирается во время выполнения. Однако, если я напишу getLevel, введите так:

getLevel : {n : _} -> Container n -> Nat

getLevel компилируется. Я знаю, что {n : _} подразумевает неограниченную множественность для n. Чего я не понимаю, так это того, как это может работать, поскольку n в Level уже удалено во время выполнения, и это то, что используется для создания значения Container n.