module Concat

data Nat : U where
    Z : Nat
    S : Nat -> Nat

infixl 7 _+_
_+_ : Nat -> Nat -> Nat
Z + m = m
S n + m = S (n + m)

infixr 3 _::_
data List : U -> U where
    Nil : {A : U} -> List A
    _::_ : {A : U} -> A -> List A -> List A

length : {A : U} -> List A -> Nat
length Nil = Z
length (x :: xs) = S (length xs)

infixl 2 _++_

_++_ : {A : U} -> List A -> List A -> List A
Nil ++ ys = ys
x :: xs ++ ys = x :: (xs ++ ys)

infixl 1 _≡_
data _≡_ : {A : U} -> A -> A -> U where
    Refl : {A : U} {a : A} -> a ≡ a

replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
replace p Refl x = x

cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
cong f Refl = Refl

thm : {A : U} (xs ys : List A) -> length (xs ++ ys) ≡ length xs + length ys
thm Nil ys = Refl
thm (x :: xs) ys = cong S (thm xs ys)