proposition: Lemma length_Sn_cons : forall (w:(list nat)) (n:nat), (length w)=(S n) -> exists (a:nat) (w':(list nat)), w = (cons a w').
proof: Proof. destruct w. intros. discriminate H. intros. exists n. exists w. trivial. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef