Require Import List.

Set Implicit Arguments.

Inductive even_length {A : Type} : list A -> Prop:=
| e_nil : even_length nil
| e_cons : forall e l, odd_length l -> even_length (e::l)
with
  odd_length {A : Type} : list A -> Prop :=
  | o_cons : forall e l, even_length l -> odd_length (e::l).

Lemma map_even : forall A B (f : A -> B) (l : list A),
    even_length l -> even_length (map f l).
Proof.
  induction l.
  (** nil *)
  - intros. simpl. econstructor.
  (** cons *)
  - intros. simpl.
    inversion_clear H.
    econstructor.
    Abort. (** odd_length l -> odd_length (map f l) would help *)

Scheme even_length_mut := Induction for even_length Sort Prop
with odd_length_mut := Induction for odd_length Sort Prop.