```
{-# 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
```