proposition: Lemma term_rect_forall : forall (P : term -> Type) (H1 : forall x, P (Var x)) (H2 : forall f v, (forall t, Inb term_eq_dec t v = true -> P t) -> P (Fun f v)), forall t, P t.
proof: Proof. intros. apply term_rect with (Q := fun v => forall t, Inb term_eq_dec t v = true -> P t); simpl. hyp. hyp. intros. discr. intros. destruct (term_eq_dec t1 t0). subst t1. hyp. apply X0. hyp. Qed.
imports: CoLoR(LogicUtil BoolUtil ListUtil EqUtil ListDec NatUtil ListMax) Coq(Peano_dec)