proposition: Lemma list_length_ind_S : 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 (n:nat) (xs:(list nat)), (lt (length xs) (S n) -> (P xs)).
proof: Proof. intros P P0 Plt. induction n. intros. assert (xs=nil). apply length_0_nil. apply lt_1_0. assumption. rewrite H0. assumption. intros. elim (lt_S_case (length xs) (S n) H). auto. intro. apply (Plt n); auto. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef