ListIndAlt.v

Lemma list_len_odd_even_ind:
  forall
    (X: Type)
    (P: list X -> Prop)
    (H: forall xs, length xs = 0 -> P xs)
    (J: forall xs, length xs = 1 -> P xs)
    (K: forall xs n, length xs = n -> P xs -> forall ys, length ys = S (S n) -> P ys)
    (l: list X),
    P l.
Proof.
  intros. cut (P l /\ forall y, P (y :: l)). tauto.
  induction l.
  split; [ apply (H []) | intro y; apply (J [y]) ]; reflexivity.
  destruct IHl as [L R].
  split.
  apply (R x).
  intros;  apply (K l (length l) refl_equal L); reflexivity.
Qed.