------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use the Data.(Nat/Fin).Induction
-- modules directly.
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Induction.Nat where

open import Data.Nat.Induction public
open import Data.Fin.Induction public