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.