fact: Fixpoint nb_symb_occs_terms n (ts : terms n) := match ts with | Vnil => 0 | Vcons u us => nb_symb_occs u + nb_symb_occs_terms us end.
imports: CoLoR(ListUtil LogicUtil EqUtil BoolUtil NatUtil VecUtil VecMax ListMax)