proposition: Lemma subterm_ind_sub : 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 v). apply subterm_eq_var. hyp. subst u. apply IH. unfold subterm. intros. destruct H0. destruct H0. destruct x. 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, Vin t v /\ subterm_eq u0 t). apply subterm_fun_elim. hyp. destruct H3. destruct H3. assert (P' x). eapply Vforall_in with (n := arity f). apply H. hyp. apply H5. hyp. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil VecUtil ListUtil BoolUtil NatUtil RelUtil)