fact: Fixpoint vars_list ts := match ts with | nil => empty | t :: ts' => union (vars t) (vars_list ts') end.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)