proposition: Lemma subterm_sub_ind : forall (P : term -> Prop) (IH : forall t, (forall u, subterm u t -> P u) -> P t), forall t u, subterm_eq u t -> P u.
proof: Proof. intros P IH. set (P' := fun t => forall u, subterm_eq u t -> P u). change (forall t, P' t). apply term_ind_forall. unfold P'. intros. assert (u = Var x). apply subterm_eq_var. hyp. subst u. apply IH. unfold subterm. intros. destruct H0. destruct H0. destruct x0. cong. discr. intros. unfold P'. intros. apply IH. intros. assert (subterm u0 (Fun f v)). eapply subterm_trans_eq2. apply H1. hyp. assert (exists t, In t v /\ subterm_eq u0 t). apply subterm_fun_elim with f. hyp. destruct H3. destruct H3. assert (P' x). apply lforall_in with term v. hyp. hyp. apply H5. hyp. Qed.
imports: CoLoR(LogicUtil) CoLoR(ListUtil)