module List where open import Bool open import Logic open import Eq infixr 40 _∷_ -- _++_ data List A : Set where [] : List A _∷_ : A → List A → List A