Require Import Arith.
Require Import List.

Fixpoint rev {A:Set} (xs:(list A)) : (list A) :=
  match xs with
    nil => nil
  | x::xs => (rev xs) ++ (x::nil)
  end.

Fixpoint nth {A:Set} (i:nat) (xs:(list A)) : (option A) :=
  match i, xs with
    i, nil => None
  | 0, (cons x xs) => (Some x)
  | (S i), (cons x xs) => (nth i xs)
  end.

Fixpoint length {A:Set} (xs: list A) : nat :=
  match xs with
  | nil => 0
  | x :: xs => S (length xs)
  end.

Lemma app_length : forall (A:Set) (xs ys: list A), length (xs ++ ys) = length xs + length ys.
Proof.

Qed.