proposition: Lemma term_ind_forall_cast : forall (P : term -> Prop) (Hvar : forall x, P (Var x)) (Hfun : forall f n (ts : terms n) (h : n = arity f), Vforall P ts -> P (Fun f (Vcast ts h))), forall t, P t.
proof: Proof. intros. apply term_ind_forall. hyp. intros. rewrite <- (Vcast_refl v (eq_refl (arity f))). apply Hfun. hyp. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)