Set Implicit Arguments.

Inductive List (a : Type) : Type :=
  | Nil : List a
  | Cons : a -> List a -> List a.

Fixpoint append (a : Type) (xs ys : List a) : List a :=
  match xs with
    | Nil => ys
    | Cons x xs => Cons x (append xs ys)
  end.

Infix "++" := append (right associativity, at level 60).

Variable (a : Type).

Lemma NilIsNil : Nil = Nil.
  Proof.
    reflexivity.
  Qed.

Lemma NilAppend (xs : List a) : xs = Nil _ ++ xs.
  Proof. 
    simpl.
    reflexivity.
  Qed.

Lemma AppendAssoc (xs ys zs : List a) : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs.
  Proof.
    induction xs.
    (*Base case*)
    simpl.
    reflexivity. 
    (*Cons case*)   
    simpl.
    rewrite IHxs.
    reflexivity.
  Qed.


Extraction Language Haskell.

Recursive Extraction append.