For Mukesh

intersperse.v

Fixpoint map_intersperse_2
         (A B : Type) (f : A -> B) (c : A) (l : list A) {struct l} :
  map f (intersperse _ c l) = intersperse _ (f c) (map f l)  :=
  match l with
  | [] => eq_refl
  | h :: t =>
    let foo := map_intersperse_2 _ _ f c t in
    match t as t0
          return
          map f (intersperse _ c t0)
          =
          intersperse _ (f c) (map f t0)
          ->
          map f (intersperse _ c (h :: t0))
          =
          intersperse _ (f c) (map f (h :: t0))
    with
    | [] => fun _ => eq_refl
    | _ :: _ => fun foo =>
    match foo in _ = X return _ = f h :: f c :: X with
    | eq_refl => eq_refl
    end
    end foo
  end.