{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProvingBasics.Termination.WellFounded where

Well-founded induction

import Padova2025.ProvingBasics.Termination.WellFounded.Base
import Padova2025.ProvingBasics.Termination.WellFounded.Scheme
import Padova2025.ProvingBasics.Termination.WellFounded.Examples