Module Existential

Meta-data

Contents

data Exists (f : Type -> Type) where
    MkExists : exists {a:Type} . f a -> Exists f