proposition: Lemma beq_fun : forall f ts g us, beq_term (Fun f ts) (Fun g us) = beq_symb f g && beq_vec beq_term ts us.
proof: Proof. intros. rewrite <- beq_terms. refl. Qed.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)