{-# OPTIONS --cubical --safe #-}

open import Prelude
open import Relation.Binary

module LexPerm where