fact: Definition vars_vec := fix vars_vec n (ts : terms n) := match ts with | Vnil => empty | Vcons u ts => union (vars u) (vars_vec _ ts) end.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)