proposition: Lemma list_length_ind : forall (P: (list nat) -> Prop), (P nil) -> (forall (n:nat), (forall (xs:(list nat)), (lt (length xs) (S n)) -> (P xs)) -> forall (xs:(list nat)), (length xs)=(S n) -> (P xs)) -> forall (xs:(list nat)), (P xs).
proof: Proof. intros. apply list_length_ind_S with (n:=(length xs)). assumption. assumption. auto with arith. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef