\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>