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