The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Below is a simple theorem I would like to prove with induction.  I have copied code up to the point where I would like to where I would like to use an inductive hypothesis.  However, Coq does not give me an inductive hypothesis.  What do I need to do to get things working?

                 - Ken

Inductive Test : Type :=
  | Leaf : nat -> Test
  | Nodes : list Test -> Test.

Fixpoint same x := match x with
                   | Leaf x => Leaf x
                   | Nodes l => Nodes (map same l)
                   end.

Theorem ss : forall x, same x = x.
Proof.
    induction x.
    unfold same. reflexivity.