See this page (https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usag...) for info on erasure. Unused proof values or indices in data types used for static checking are erased at compile time via usage analysis (if you don't use it in the RHS of a function definition, it gets erased).

If you want to ensure that the indices of your data type or arguments to your function are erased, you can use the new dot notation. E.g., if you give a function called "half" the following type

  half : (n : Nat) -> .(pf : Even n) -> Nat

then the compiler will complain if the proof argument is actually used.