David's proposal:

1) Assuming the following definition:

   Require Import List.

   Inductive Term : Set :=
   | var : nat -> Term
   | apply : nat -> list Term -> Term.

Prove this alternative induction principle:

Lemma Term_ind' :
   forall P : Term -> Prop,
   (forall x, P (var x)) ->
   (forall f args, (forall t, In t args -> P t) -> P (apply f args)) ->
   forall t : Term, P t.

2) Illustrate its use on an example of your choice.

--

David's answer:

Require Import List.

Inductive Term : Set :=
| var : nat -> Term
| apply : nat -> list Term -> Term.

Lemma Term_ind2 :
   forall P : Term -> Prop,
   forall Q : list Term -> Prop,
   Q nil ->
   (forall t args, P t -> Q args -> Q (t::args)) ->
   (forall x, P (var x)) ->
   (forall f args, Q args -> P (apply f args)) ->
   forall t : Term, P t.
Proof.
fix 7.
intros.
destruct t as [x | f args].
apply H1.
apply H2.
revert args.
fix list_Term_ind2 1.
intro.
destruct args as [ | t args'].
assumption.
apply H0.
apply Term_ind2 with Q; assumption.
apply list_Term_ind2.
Show Proof.
Qed.

Lemma Term_ind' :
   forall P : Term -> Prop,
   (forall x, P (var x)) ->
   (forall f args, (forall t, In t args -> P t) -> P (apply f args)) ->
   forall t : Term, P t.
Proof.
intros.
apply Term_ind2 with (fun args => forall t, In t args -> P t).
intros.
inversion H1.
simpl.
intros.
destruct H3.
rewrite <- H3.
assumption.
apply H2.
assumption.
assumption.
assumption.
Qed.

Inductive Occur (x:nat) : Term -> Prop :=
| o_var : Occur x (var x)
| o_apply : forall t f args, In t args -> Occur x t -> Occur x (apply  
f args).

Inductive NotOccur (x:nat) : Term -> Prop :=
| no_var : forall y, x<>y -> NotOccur x (var y)
| no_apply :
     forall f args, (forall t, In t args -> NotOccur x t) -> NotOccur  
x (apply f args).

Theorem notoccur_not_occur : forall x t, NotOccur x t -> ~Occur x t.
Proof.
induction t using Term_ind'; intro.
inversion_clear H.
swap H0.
inversion_clear H.
reflexivity.
inversion_clear H0.
intro.
inversion_clear H0.
apply H with t; auto.
Qed.

--

Reynald's comment:

Require Import List.

(*
Inductive Term : Set :=
| var : nat -> Term
| apply : nat -> list Term -> Term.
*)

Inductive Term : Set :=
| var : nat -> Term
| apply : nat -> List -> Term
with List : Set :=
| Nil : List
| Cons : Term -> List -> List.

Scheme Term_ind1 := Induction for Term Sort Prop
  with Term_ind2 := Induction for List Sort Prop.

Print Term_ind1.

Fixpoint IN (t:Term) (L:List) {struct L} : Prop :=
  match L with 
    | Nil => False
    | Cons Hd Tl => Hd = t \/ IN t Tl
  end.
  
Lemma Term_ind' : 
  forall P : Term -> Prop,
    (forall x, P (var x)) ->
    (forall f args, (forall t, IN t args -> P t) -> P (apply f args)) -> 
    forall t: Term, P t.
intros.
elim t using Term_ind1 with (P0 := fun l:List => (forall t, (IN t l) -> P t)).
auto.
intros.
apply H0.
auto.
intros.
simpl in H1.
contradiction.
intros.
simpl in H3.
inversion_clear H3.
subst t0.
auto.
apply H2.
auto.
Qed.