module klaus where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero + n = n
(suc n) + m = suc (n + m)

data Vec(A : Set) : Nat -> Set where
  [] : Vec A zero
  _::_ : ∀ {n} -> A -> Vec A n -> Vec A (suc n)

concat : ∀ {A n m} -> Vec A n -> Vec A m -> Vec A (n + m)
concat [] v = v
concat (x :: xs) v = x :: (concat xs v)

head : ∀ {A n} -> Vec A (suc n) -> A
head (x :: xs) = x

infix 4 _==_

data _==_ {A : Set}(x : A) : A -> Set where
    refl : x == x

sym : ∀ {A : Set} {a b : A} -> a == b -> b == a
sym refl = refl

trans : {A : Set}{a b c : A} -> a == b -> b == c -> a == c
trans refl refl = refl

cong : {A B : Set} {a b : A } -> (f : A -> B) -> a == b -> f a == f b
cong f refl = refl

+-assoc : ∀ n m p -> n + (m + p) == (n + m) + p
+-assoc zero m p = refl
+-assoc (suc n) m p = cong suc (+-assoc n m p)