----------------------------------------------------------------------------------------------------
-- Extensional Wellfounded orders
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

module ExtensionalWellfoundedOrder.Everything where

{- Definition -}
open import ExtensionalWellfoundedOrder.Base public

{- Arithmetic operations -}
open import ExtensionalWellfoundedOrder.Arithmetic public