{-# OPTIONS --without-K --safe #-} module Data.Fin.Indexed where open import Data.Fin.Indexed.Base public