module My.SetTheory.Induction where

-- §──────────────────────────────────────────────────────────────────
-- Required modules
-- §──────────────────────────────────────────────────────────────────

import My.SetTheory.Induction.WellFounded as MySTIWF
import My.SetTheory.Induction.NoInfiniteDescent as MySTINID
import My.SetTheory.Induction.Nat as MySTIN

open MySTIWF public
open MySTINID public
open MySTIN public