proposition: Lemma term_ind_forall2 : forall (P : term -> Prop) (H1 : forall x, P (Var x)) (H2 : forall f v, (forall t, In t v -> P t) -> P (Fun f v)), forall t, P t.
proof: Proof. intros. apply term_ind with (Q := fun v => forall t, In t v -> P t); simpl. hyp. hyp. intros. contr. intros. destruct H3. subst. hyp. apply H0. hyp. Qed.
imports: CoLoR(LogicUtil BoolUtil ListUtil EqUtil ListDec NatUtil ListMax) Coq(Peano_dec)