pe200012

open import Level                                      using (_⊔_)
open import Function                                   using (_∘_)
open import Data.Vec                                   using (Vec; []; _∷_; foldr)
open import Data.Nat                                   using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties.Simple                 using (+-right-identity; +-suc)
open import Data.Sum                                   using (_⊎_; inj₁; inj₂)
open import Data.Product                               using (∃; _×_; _,_; proj₁; proj₂)
open import Data.Empty                                 using (⊥-elim)
open import Relation.Nullary                           using (Dec; yes; no; ¬_)
open import Relation.Binary                            using (module DecTotalOrder; DecTotalOrder; Rel)