Documentation

data Finite# (a :: Nat) :: TYPE R #

weaken :: forall (n :: Nat). Finite# n -> Fin# n #