{- ∀(a : Type) → a -}

1