\begin{code} {-# OPTIONS --cubical --safe #-} module Cardinality.Finite.SplitEnumerable.Container where open import Prelude open import Container open import Container.List open import Data.Fin open import Container.Membership (ℕ , Fin) open import Path.Reasoning open import Data.Sigma.Properties open import Function.Surjective.Properties open import Data.Fin.Properties ℰ! : Type a → Type a \end{code} %<*split-enum-def> \begin{code} ℰ! A = Σ[ support ⦂ List A ] ((x : A) → x ∈ support) \end{code} %</split-enum-def>