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