proposition: Lemma term_ind_forall : forall (P : term -> Prop) (H1 : forall v, P (Var v)) (H2 : forall f v, Vforall P v -> P (Fun f v)), forall t, P t.
proof: Proof. intros. apply term_ind with (Q := Vforall P). exact H1. exact H2. exact I. intros. simpl. split; hyp. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)