Induction principle for nested inductive types

Question

I noticed that I keep redefining very similar induction principles for nested (and sometime mutually) inductive types because the one generated automatically by Coq is too weak. Here is a very simplified example:

Require Import Coq.Lists.List.

Inductive T : Set :=
| C1 : T
| C2 : list T -> T.

Section T_nested_ind.
  Variable P : T -> Prop.
  Hypothesis C1_case : P C1.
  Hypothesis C2_case : forall l : list T, Forall P l -> P (C2 l).

  Fixpoint T_nested_ind (t : T) :=
    match t with
    | C1 => C1_case
    | C2 xs =>
        let H := (fix fold (xs : list T) : Forall P xs :=
          match xs with
          | nil => Forall_nil _
          | x :: xs => Forall_cons _ (T_nested_ind x) (fold xs)
          end) xs in
        C2_case xs H
    end.
End T_nested_ind.

Coq generates automatically T_ind:

forall P : T -> Prop,
  P C1 ->
  (forall l : list T, P (C2 l)) ->
  forall t : T, P t

While I need an induction hypothesis for the elements nested in the list T_nested_ind:

forall P : T -> Prop,
  P C1 ->
  (forall l : list T, Forall P l -> P (C2 l)) ->
  forall t : T, P t

1. Is there a way to automate this?
2. Am I doing something wrong, if I need such an induction principle?
3. What is the standard solution in Coq?
4. Is there some incubating research on the subject?

Answer 1

Here's a partial answer:

2. No, Coq is giving you an induction principle which is correct but not very useful, and you can do better with a clever use of fix as you already know.
3. As far as I know, defining and proving a new induction principle is the standard solution.