{-# OPTIONS --with-K #-} module Prelude.Irrelevance.List where open import Prelude.Irrelevance.List.Unique public open import Prelude.Irrelevance.List.Membership public open import Prelude.Irrelevance.List.Permutation public