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

良基歸納#

import Padova2025-zh-TW.ProvingBasics.Termination.WellFounded.Base
import Padova2025-zh-TW.ProvingBasics.Termination.WellFounded.Scheme
import Padova2025-zh-TW.ProvingBasics.Termination.WellFounded.Examples