proposition: Lemma term_int_eq : forall xint1 xint2 t, (forall x, In x (vars t) -> xint1 x = xint2 x) -> term_int xint1 t = term_int xint2 t.
proof: Proof. intros xint1 xint2 t. pattern t; apply term_ind_forall; clear t; intros. simpl. apply H. simpl. intuition. apply (f_equal (fint I f)). apply Vmap_eq. apply Vforall_intro. intros. apply (Vforall_in H H1). intros. apply H0. rewrite vars_fun. apply (vars_vec_in H2 H1). Qed.
imports: Coq(List) CoLoR(LogicUtil NaryFunction VecUtil VecMax NatUtil)