----------------------------------------------------------------------------------------------------
-- Marked Extensional Wellfounded orders (without transitivity)
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}
module MEWO.Everything where

open import Relation.Closure

open import MEWO.Base
open import MEWO.Covered
open import MEWO.Constructions
open import MEWO.TranslationV